src/HOL/MicroJava/J/JListExample.thy
2012-02-17 wenzelm 2012-02-17 simplified configuration options for syntax ambiguity;
2012-02-16 wenzelm 2012-02-16 simplified configuration options for syntax ambiguity;
2011-12-13 wenzelm 2011-12-13 modernized specifications;
2011-10-21 bulwahn 2011-10-21 replacing code_inline by code_unfold, removing obsolete code_unfold, code_inline del now that the ancient code generator is removed
2011-08-05 Andreas Lochbihler 2011-08-05 replace old SML code generator by new code generator in MicroJava/J
2010-09-03 wenzelm 2010-09-03 configuration options Syntax.ambiguity_enabled (inverse of former Syntax.ambiguity_is_error), Syntax.ambiguity_level (with Isar attribute "syntax_ambiguity_level"), Syntax.ambiguity_limit;
2010-03-01 haftmann 2010-03-01 replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
2009-08-11 haftmann 2009-08-11 temporary adjustment to dubious state of eta expansion in recfun_codegen
2008-10-07 haftmann 2008-10-07 arbitrary is undefined
2007-09-30 wenzelm 2007-09-30 avoid internal names;
2007-08-28 berghofe 2007-08-28 Code generator now uses sequences with depth limit.
2007-05-10 haftmann 2007-05-10 consts in consts_code Isar commands are now referred to by usual term syntax
2006-01-14 wenzelm 2006-01-14 generated code: raise Match instead of ERROR;
2005-08-25 berghofe 2005-08-25 Adapted to new code generator syntax.
2005-07-12 berghofe 2005-07-12 Auxiliary functions to be used in generated code are now defined using "attach".
2005-06-17 haftmann 2005-06-17 migrated theory headers to new format
2005-02-13 skalberg 2005-02-13 Deleted Library.option type.
2003-04-01 nipkow 2003-04-01 Made empty a translation rather than a constant.
2002-10-23 streckem 2002-10-23 Added compiler
2002-04-19 berghofe 2002-04-19 wf is no longer implemented by true (due to change in definition of class_rec).
2002-02-26 kleing 2002-02-26 introduces SystemClasses and BVExample
2002-02-21 kleing 2002-02-21 new document
2001-12-20 berghofe 2001-12-20 Eliminated "query" syntax.
2001-12-20 berghofe 2001-12-20 cast_ok no longer disabled (thanks to improvement of code generator).
2001-12-10 berghofe 2001-12-10 Example for code generator.