src/HOL/Auth/Guard/Extensions.thy
2014-11-01 wenzelm 2014-11-01 eliminated spurious semicolons;
2014-09-11 blanchet 2014-09-11 renamed 'datatype' to 'old_datatype'; 'datatype' is now alias for 'datatype_new'
2014-04-24 haftmann 2014-04-24 avoid non-standard simp default rule
2014-02-12 blanchet 2014-02-12 adapted to 'xxx_{case,rec}' renaming, to new theorem names, and to new variable names in theorems * * * more transition of 'xxx_rec' to 'rec_xxx' and same for case * * * compile * * * 'rename_tac's to avoid referring to generated names * * * more robust scripts with 'rename_tac' * * * 'where' -> 'of' * * * 'where' -> 'of' * * * renamed 'xxx_rec' to 'rec_xxx'
2011-12-28 wenzelm 2011-12-28 reverted some changes for set->predicate transition, according to "hg log -u berghofe -r Isabelle2007:Isabelle2008"; tuned proofs;
2011-11-20 wenzelm 2011-11-20 'lemmas' / 'theorems' commands allow 'for' fixes and standardize the result before storing;
2011-09-12 nipkow 2011-09-12 new fastforce replacing fastsimp - less confusing name
2011-02-18 wenzelm 2011-02-18 standardized headers;
2010-09-08 haftmann 2010-09-08 modernized primrec
2010-03-01 krauss 2010-03-01 killed recdefs in HOL-Auth
2010-03-01 haftmann 2010-03-01 replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
2009-09-21 haftmann 2009-09-21 adapted proof
2008-05-07 berghofe 2008-05-07 - Instantiated parts_insert_substD to avoid problems with HO unification - Replaced auto by fastsimp in proof of parts_invKey, since auto looped because of the new encoding of sets
2006-11-17 wenzelm 2006-11-17 more robust syntax for definition/abbreviation/notation;
2006-09-28 wenzelm 2006-09-28 replaced syntax/translations by abbreviation;
2006-07-26 webertj 2006-07-26 linear arithmetic splits certain operators (e.g. min, max, abs)
2006-03-10 haftmann 2006-03-10 renamed HOL + - * etc. to HOL.plus HOL.minus HOL.times etc.
2006-01-03 paulson 2006-01-03 Provers/classical: stricter checks to ensure that supplied intro, dest and elim rules are well-formed
2005-09-28 paulson 2005-09-28 streamlined theory; conformance to recent publication
2005-06-17 haftmann 2005-06-17 migrated theory headers to new format
2004-10-11 nipkow 2004-10-11 Proofs needed to be updated because induction now preserves name of induction variable.
2003-12-21 paulson 2003-12-21 tidying of HOL/Auth esp Guard lemmas
2003-12-21 nipkow 2003-12-21 removed insert_Diff_single from simpset because it interfered with Auth :-(
2002-09-30 nipkow 2002-09-30 modified induct method
2002-08-21 paulson 2002-08-21 Frederic Blanqui's new "guard" examples