src/HOL/MicroJava/J/Example.thy
2007-09-30 wenzelm 2007-09-30 avoid internal names;
2007-07-30 wenzelm 2007-07-30 tuned ML declarations;
2007-07-21 wenzelm 2007-07-21 tactics: avoid dynamic reference to accidental theory context (via ML_Context.the_context etc.);
2007-07-11 berghofe 2007-07-11 - Renamed inductive2 to inductive - Renamed some theorems about transitive closure for predicates
2007-02-07 berghofe 2007-02-07 Adapted to new inductive definition package.
2006-11-17 wenzelm 2006-11-17 more robust syntax for definition/abbreviation/notation;
2006-09-28 wenzelm 2006-09-28 replaced syntax/translations by abbreviation;
2005-06-17 haftmann 2005-06-17 migrated theory headers to new format
2004-11-22 nipkow 2004-11-22 fixed proof
2003-05-26 streckem 2003-05-26 Introduced distinction wf_prog vs. ws_prog
2002-02-26 kleing 2002-02-26 introduces SystemClasses and BVExample
2002-02-21 kleing 2002-02-21 new document
2001-12-16 kleing 2001-12-16 exception merge, cleanup, tuned
2001-10-23 wenzelm 2001-10-23 eliminated old numerals;
2001-10-05 wenzelm 2001-10-05 sane numerals (stage 1): added generic 1, removed 1' and 2 on nat, "num" syntax (still with "#"), Numeral0, Numeral1;
2001-10-01 streckem 2001-10-01 Added axiom e~=This to reflect strengthened precond. in rule LAss
2001-06-12 oheimb 2001-06-12 corrected xsymbol/HTML syntax
2001-02-05 oheimb 2001-02-05 improved document (added headers etc)
2001-02-01 oheimb 2001-02-01 converted to Isar, simplifying recursion on class hierarchy
2001-01-02 oheimb 2001-01-02 added type annotation to Call
2000-12-06 oheimb 2000-12-06 improved superclass entry for classes and definition status of is_class, class corrected recursive definitions of "method" and "fields" cleanup of many proofs, removed superfluous tactics and theorems
2000-10-17 oheimb 2000-10-17 cosmetics
2000-09-21 kleing 2000-09-21 unsymbolized
2000-09-01 wenzelm 2000-09-01 isatool nonascii;
2000-08-02 oheimb 2000-08-02 minor corrections
2000-07-14 oheimb 2000-07-14 corrections (cast relation, Prog.ML -> Decl.ML)
2000-07-14 oheimb 2000-07-14 re-structuring MicroJava; added Example; corrected := syntax; simplfied cast