src/HOL/MicroJava/J/TypeRel.thy
2008-10-07 haftmann 2008-10-07 arbitrary is undefined
2007-07-11 berghofe 2007-07-11 - Renamed inductive2 to inductive - Renamed some theorems about transitive closure for predicates
2007-04-04 wenzelm 2007-04-04 rebind HOL.refl as refl (hidden by widen.refl);
2007-02-07 berghofe 2007-02-07 Adapted to new inductive definition package.
2006-10-11 haftmann 2006-10-11 added code lemma
2006-01-04 nipkow 2006-01-04 Reversed Larry's option/iff change.
2005-12-21 paulson 2005-12-21 removed or modified some instances of [iff]
2005-06-17 haftmann 2005-06-17 migrated theory headers to new format
2004-06-16 paulson 2004-06-16 removal of x-symbol syntax <Sigma> for dependent products
2003-08-28 skalberg 2003-08-28 Extended the notion of letter and digit, such that now one may use greek, gothic, euler, or calligraphic letters as normal letters.
2003-07-25 nipkow 2003-07-25 Replaced \<leadsto> by \<rightharpoonup>
2003-05-26 streckem 2003-05-26 Introduced distinction wf_prog vs. ws_prog
2002-04-19 berghofe 2002-04-19 Improved definition of class_rec: no longer mixes algorithm and termination check.
2002-02-21 kleing 2002-02-21 new document
2001-12-16 kleing 2001-12-16 exception merge, cleanup, tuned
2001-12-10 berghofe 2001-12-10 Turned subcls1 into an inductive relation to make it executable.
2001-10-30 wenzelm 2001-10-30 tuned induct proofs;
2001-06-12 oheimb 2001-06-12 corrected xsymbol/HTML syntax
2001-05-04 nipkow 2001-05-04 made same_fst recdef_simp
2001-04-24 oheimb 2001-04-24 simplified proofs concerning class_rec
2001-02-09 wenzelm 2001-02-09 tuned;
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
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-03 wenzelm 2000-10-03 eliminated \<oplus>;
2000-09-22 kleing 2000-09-22 added HTML syntax; added spaces in normal syntax for better documents
2000-09-21 kleing 2000-09-21 unsymbolized
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
2000-07-05 oheimb 2000-07-05 corrected symbol for casting relation
2000-01-05 oheimb 2000-01-05 improved symbol for subcls relation
2000-01-03 oheimb 2000-01-03 removed inj_eq from the default simpset again
1999-11-26 nipkow 1999-11-26 Various little changes like cmethd -> method and cfield -> field.
1999-11-11 nipkow 1999-11-11 *** empty log message ***