src/HOL/MicroJava/J/WellForm.thy
2010-03-01 ago replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
2009-11-24 ago backported parts of abstract byte code verifier from AFP/Jinja
2009-11-12 ago Remove map_compose, replaced by map_map
2009-10-17 ago eliminated hard tabulators, guessing at each author's individual tab-width;
2007-07-11 ago - Renamed inductive2 to inductive
2007-04-11 ago tuned
2007-02-07 ago Adapted to new inductive definition package.
2006-01-04 ago Reversed Larry's option/iff change.
2005-12-21 ago removed or modified some instances of [iff]
2005-06-17 ago migrated theory headers to new format
2005-02-01 ago the new subst tactic, by Lucas Dixon
2004-08-02 ago Modifications for trancl_tac (new solver in simplifier).
2004-07-26 ago New prover for transitive and reflexive-transitive closure of relations.
2003-08-29 ago Methods rule_tac etc support static (Isar) contexts.
2003-05-26 ago Introduced distinction wf_prog vs. ws_prog
2003-05-14 ago *** empty log message ***
2002-10-23 ago Added compiler
2002-09-26 ago Converted Fun to Isar style.
2002-03-09 ago in wellformed programs, exceptions are classes
2002-02-26 ago introduces SystemClasses and BVExample
2002-02-21 ago new document
2001-12-20 ago renamed rtrancl_into_rtrancl2 to converse_rtrancl_into_rtrancl
2001-12-16 ago exception merge, cleanup, tuned
2001-02-05 ago improved document (added headers etc)
2001-02-01 ago converted to Isar, simplifying recursion on class hierarchy
2000-12-06 ago improved superclass entry for classes and definition status of is_class, class
2000-09-25 ago untabified for HTML
2000-09-22 ago added HTML syntax; added spaces in normal syntax for better documents
2000-09-21 ago unsymbolized
2000-01-05 ago improved symbol for subcls relation
2000-01-03 ago removed inj_eq from the default simpset again
1999-11-26 ago Various little changes like cmethd -> method and cfield -> field.
1999-11-11 ago *** empty log message ***