src/HOL/MicroJava/J/JTypeSafe.thy
2011-10-12 ago modernized structure Induct_Tacs;
2011-01-16 ago tuned headers;
2010-09-06 ago more antiquotations;
2009-11-24 ago backported parts of abstract byte code verifier from AFP/Jinja
2009-08-13 ago Removal of redundant settings of unification trace and search bounds.
2009-07-23 ago renamed simpset_of to global_simpset_of, and local_simpset_of to simpset_of -- same for claset and clasimpset;
2008-06-14 ago simplified InductTacs.case_tac/induct_tac;
2008-06-10 ago tuned proofs;
2008-06-09 ago DatatypePackage.case_tac;
2007-08-07 ago turned Unify flags into configuration options (global only);
2007-07-21 ago tactics: avoid dynamic reference to accidental theory context (via ML_Context.the_context etc.);
2007-07-11 ago - Renamed inductive2 to inductive
2007-02-07 ago Adapted to new inductive definition package.
2005-06-17 ago migrated theory headers to new format
2003-08-08 ago Changed lemmas .._type_sound
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-02-26 ago introduces SystemClasses and BVExample
2002-02-21 ago new document
2002-02-14 ago nodups -> distinct
2001-12-16 ago exception merge, cleanup, tuned
2001-10-01 ago Removed some unfoldings of defs after declaring wf_java_prog as syntax
2001-02-05 ago improved document (added headers etc)
2001-02-01 ago converted to Isar, simplifying recursion on class hierarchy
1999-11-11 ago *** empty log message ***