src/HOL/MicroJava/J/WellForm.thy
2007-04-11 haftmann 2007-04-11 tuned
2007-02-07 berghofe 2007-02-07 Adapted to new inductive definition package.
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
2005-02-01 paulson 2005-02-01 the new subst tactic, by Lucas Dixon
2004-08-02 ballarin 2004-08-02 Modifications for trancl_tac (new solver in simplifier).
2004-07-26 ballarin 2004-07-26 New prover for transitive and reflexive-transitive closure of relations. - Code in Provers/trancl.ML - HOL: Simplifier set up to use it as solver
2003-08-29 ballarin 2003-08-29 Methods rule_tac etc support static (Isar) contexts.
2003-05-26 streckem 2003-05-26 Introduced distinction wf_prog vs. ws_prog
2003-05-14 nipkow 2003-05-14 *** empty log message ***
2002-10-23 streckem 2002-10-23 Added compiler
2002-09-26 paulson 2002-09-26 Converted Fun to Isar style. Moved Pi, funcset, restrict from Fun.thy to Library/FuncSet.thy. Renamed constant "Fun.op o" to "Fun.comp"
2002-03-09 kleing 2002-03-09 in wellformed programs, exceptions are classes
2002-02-26 kleing 2002-02-26 introduces SystemClasses and BVExample
2002-02-21 kleing 2002-02-21 new document
2001-12-20 nipkow 2001-12-20 renamed rtrancl_into_rtrancl2 to converse_rtrancl_into_rtrancl
2001-12-16 kleing 2001-12-16 exception merge, cleanup, 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-09-25 kleing 2000-09-25 untabified for HTML
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-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 ***