src/HOL/MicroJava/JVM/JVMListExample.thy
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
2008-09-29 wenzelm 2008-09-29 code example: back to individual ML commands, which are now thread-safe;
2007-09-30 wenzelm 2007-09-30 avoid internal names;
2007-08-20 wenzelm 2007-08-20 theory header: more precise imports;
2007-08-10 haftmann 2007-08-10 dropped code generator setup garbage
2007-07-30 wenzelm 2007-07-30 tuned ML declarations;
2007-05-10 haftmann 2007-05-10 consts in consts_code Isar commands are now referred to by usual term syntax
2006-11-17 wenzelm 2006-11-17 more robust syntax for definition/abbreviation/notation;
2006-10-31 haftmann 2006-10-31 adapted to new serializer syntax
2006-10-20 haftmann 2006-10-20 slight cleanup
2006-10-11 haftmann 2006-10-11 added code generator setup
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-07-01 berghofe 2005-07-01 Corrected implementation of arbitrary on cname.
2005-06-17 haftmann 2005-06-17 migrated theory headers to new format
2002-04-30 kleing 2002-04-30 tuned
2002-04-19 berghofe 2002-04-19 wf is no longer implemented by true (due to change in definition of class_rec).
2002-03-09 kleing 2002-03-09 canonical start state
2002-02-28 kleing 2002-02-28 fixed missing label
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 cast_ok and match_exception_entry no longer disabled (thanks to improvement of code generator).
2001-12-17 kleing 2001-12-17 fixed JVMListExample
2001-12-16 kleing 2001-12-16 exception merge, doesn't work yet
2001-12-10 berghofe 2001-12-10 Example for code generator.