src/HOL/MicroJava/J/WellType.thy
2016-01-11 wenzelm 2016-01-11 eliminated old defs;
2016-01-02 wenzelm 2016-01-02 isabelle update_cartouches -c -t;
2015-10-07 wenzelm 2015-10-07 isabelle update_cartouches;
2014-11-02 wenzelm 2014-11-02 modernized header;
2014-09-09 blanchet 2014-09-09 ported MicroJava to new datatypes
2011-04-23 wenzelm 2011-04-23 modernized specifications;
2010-09-28 haftmann 2010-09-28 modernized primrecs
2010-03-01 haftmann 2010-03-01 replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
2010-02-11 wenzelm 2010-02-11 modernized translations;
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.
2005-06-17 haftmann 2005-06-17 migrated theory headers to new format
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-10-23 streckem 2002-10-23 Added compiler
2002-02-21 kleing 2002-02-21 new document
2002-02-14 nipkow 2002-02-14 nodups -> distinct
2001-12-16 kleing 2001-12-16 exception merge, cleanup, tuned
2001-10-01 streckem 2001-10-01 - declared wf_java_prog as syntax (previously: definition) - in wf_java_mdecl: added preconditions for 'This' - rule LAss: precondition v ~=This
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-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-07-04 oheimb 2000-07-04 added BinOp
2000-02-01 wenzelm 2000-02-01 eliminated nonascii;
2000-01-05 oheimb 2000-01-05 simplified definition of appl_methds, removing m_head
2000-01-04 oheimb 2000-01-04 new arg type for max_spec etc.
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 ***