Actually, there is a third code generator hidden somewhere in Isabelle. - Steven
On 21.07.2011, at 12:18, Lukas Bulwahn wrote: > 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. > Commands to invoke it were code_module and code_library. > > 2. A generic code generator in Isabelle by Florian Haftmann - extenible to > multiple target languages, supporting type classes, basic integration of > reflection and abstraction mechanisms > Commands to invoke it are export_code, value, code_reflect, and some others. > > > The second subsumes the first, so we intend to remove the first code > generator from the next Isabelle distribution if there are not any strong > defenders of the ancient code generator. > > > Any thoughts? > > > Lukas > > > _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
