src/HOL/MicroJava/JVM/JVMListExample.thy
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.