src/HOL/Auth/Guard/Guard.thy
2014-11-02 wenzelm 2014-11-02 modernized header uniformly as section;
2014-09-09 blanchet 2014-09-09 rename_tac'd scripts
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-11-20 wenzelm 2011-11-20 'lemmas' / 'theorems' commands allow 'for' fixes and standardize the result before storing;
2011-02-18 wenzelm 2011-02-18 standardized headers;
2010-06-28 haftmann 2010-06-28 dropped ancient infix mem
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)
2007-10-21 nipkow 2007-10-21 Eliminated most of the neq0_conv occurrences. As a result, many theorems had to be rephrased with ~= 0 instead of > 0.
2007-07-11 berghofe 2007-07-11 Adapted to new inductive definition package.
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-03-10 haftmann 2006-03-10 renamed HOL + - * etc. to HOL.plus HOL.minus HOL.times etc.
2005-08-16 nipkow 2005-08-16 name fix
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
2002-08-21 paulson 2002-08-21 Frederic Blanqui's new "guard" examples