src/HOL/MicroJava/J/JTypeSafe.thy
2015-10-13 haftmann 2015-10-13 prod_case as canonical name for product type eliminator
2015-10-07 wenzelm 2015-10-07 isabelle update_cartouches;
2015-07-18 wenzelm 2015-07-18 prefer tactics with explicit context;
2015-03-27 wenzelm 2015-03-27 tuned signature;
2015-03-25 wenzelm 2015-03-25 prefer local fixes;
2015-03-24 wenzelm 2015-03-24 clarified case_tac fixes and context;
2015-02-10 wenzelm 2015-02-10 proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.; occasionally clarified use of context;
2014-11-10 wenzelm 2014-11-10 proper context for assume_tac (atac remains as fall-back without context);
2014-11-02 wenzelm 2014-11-02 modernized header;
2014-11-01 wenzelm 2014-11-01 eliminated spurious semicolons;
2014-09-09 blanchet 2014-09-09 ported MicroJava to new datatypes
2014-06-11 Thomas Sewell 2014-06-11 Hypsubst preserves equality hypotheses Fixes included for various theories affected by this change.
2013-12-14 wenzelm 2013-12-14 proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.; clarified tool context in some boundary cases;
2013-04-27 wenzelm 2013-04-27 uniform Proof.context for hyp_subst_tac;
2013-04-18 wenzelm 2013-04-18 simplifier uses proper Proof.context instead of historic type simpset;
2013-04-10 wenzelm 2013-04-10 added ML antiquotation @{theory_context};
2013-02-28 wenzelm 2013-02-28 marginalized historic strip_tac;
2011-10-12 wenzelm 2011-10-12 modernized structure Induct_Tacs;
2011-01-16 wenzelm 2011-01-16 tuned headers;
2010-09-06 wenzelm 2010-09-06 more antiquotations;
2009-11-24 haftmann 2009-11-24 backported parts of abstract byte code verifier from AFP/Jinja
2009-08-13 paulson 2009-08-13 Removal of redundant settings of unification trace and search bounds.
2009-07-23 wenzelm 2009-07-23 renamed simpset_of to global_simpset_of, and local_simpset_of to simpset_of -- same for claset and clasimpset;
2008-06-14 wenzelm 2008-06-14 simplified InductTacs.case_tac/induct_tac;
2008-06-10 wenzelm 2008-06-10 tuned proofs;
2008-06-09 wenzelm 2008-06-09 DatatypePackage.case_tac;
2007-08-07 wenzelm 2007-08-07 turned Unify flags into configuration options (global only);
2007-07-21 wenzelm 2007-07-21 tactics: avoid dynamic reference to accidental theory context (via ML_Context.the_context etc.);
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-08-08 streckem 2003-08-08 Changed lemmas .._type_sound
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-02-26 kleing 2002-02-26 introduces SystemClasses and BVExample
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 Removed some unfoldings of defs after declaring wf_java_prog as 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
1999-11-11 nipkow 1999-11-11 *** empty log message ***