Re: [isabelle-dev] [isabelle] Code generation in Isabelle

2011-07-24 Thread Makarius
On Thu, 21 Jul 2011, Lukas Bulwahn wrote: at the moment, we have two code generators in Isabelle: 1. An ancient code generator in Isabelle by Stefan Berghofer - limited to SML without supporting type classes. Commands to invoke it were code_module and code_library. 2. A generic code

Re: [isabelle-dev] [isabelle] Code generation in Isabelle

2011-07-24 Thread Lukas Bulwahn
On 07/24/2011 04:57 PM, Makarius wrote: On Thu, 21 Jul 2011, Lukas Bulwahn wrote: at the moment, we have two code generators in Isabelle: 1. An ancient code generator in Isabelle by Stefan Berghofer - limited to SML without supporting type classes. Commands to invoke it were code_module and

Re: [isabelle-dev] [isabelle] Code generation in Isabelle

2011-07-21 Thread Burkhart Wolff
We moved recently to the new code-generator. Burkhart Am 21.07.2011 um 12:18 schrieb Lukas Bulwahn: Hello all, at the moment, we have two code generators in Isabelle: 1. An ancient code generator in Isabelle by Stefan Berghofer - limited to SML without supporting type classes.