[isabelle-dev] BNF: dead or alive?

2014-11-21 Thread Christian Sternagel
Dear list, sorry for the subject ;) René and I are currently at adapting the Show(_Generator) entry of the AFP to the new datatype package. And again we stumbled across some difficulties we already encountered when adapting the Order_Generator (and which are not resolved yet). I think it

Re: [isabelle-dev] BNF: dead or alive?

2014-11-21 Thread Dmitriy Traytel
Hi Christian, On 21.11.2014 14:09, Christian Sternagel wrote: Dear list, sorry for the subject ;) René and I are currently at adapting the Show(_Generator) entry of the AFP to the new datatype package. And again we stumbled across some difficulties we already encountered when adapting the

Re: [isabelle-dev] BNF: dead or alive?

2014-11-21 Thread Christian Sternagel
Hi Dmitriy, thanks for another round of clarification (I should really reread old emails before referring to them). On 11/21/2014 02:43 PM, Dmitriy Traytel wrote: In general, why not create map-functions that allow to map over *all* type parameters. (As I understand it, this was done just a

Re: [isabelle-dev] BNF: dead or alive?

2014-11-21 Thread Dmitriy Traytel
On 21.11.2014 15:00, Christian Sternagel wrote: Hi Dmitriy, thanks for another round of clarification (I should really reread old emails before referring to them). On 11/21/2014 02:43 PM, Dmitriy Traytel wrote: In general, why not create map-functions that allow to map over *all* type

Re: [isabelle-dev] Proposal for localized interpretations

2014-11-21 Thread Jasmin Christian Blanchette
Hi Makarius, I would expect that if Jasmin's plugin manager is also used in the code generator, it would be easy to implement plugin selection for code_datatype, too. This should work out easily with the unified Plugin_Name and Plugin concept of

Re: [isabelle-dev] Abbreviations and find_theorems

2014-11-21 Thread Makarius
On Sat, 15 Nov 2014, Gerwin Klein wrote: I agree that it would be nice to support that, esp since find_theorems is supposed to help beginners find things. Applying underscores will have unwanted side effects for other terms, esp constants, though, so one would have to be careful to apply