src/HOL/Auth/Kerberos_BAN.thy
2014-11-02 wenzelm 2014-11-02 modernized header uniformly as section;
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-05-12 blanchet 2011-05-12 Metis doesn't find an old proof in acceptable time now that higher-order equality reasoning is supported -- tuned proof script to help it
2010-09-09 paulson 2010-09-09 Tidied up proofs using sledgehammer, also deleting unnecessary semicolons
2010-07-22 wenzelm 2010-07-22 updated some headers;
2010-05-12 wenzelm 2010-05-12 modernized specifications;
2009-10-17 wenzelm 2009-10-17 eliminated hard tabulators, guessing at each author's individual tab-width; tuned headers;
2009-08-26 paulson 2009-08-26 Simplified some proofs using metis.
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-10-20 chaieb 2007-10-20 fixed proofs
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-02-01 paulson 2006-02-01 new and updated protocol proofs by Giamp Bella
2005-06-17 haftmann 2005-06-17 migrated theory headers to new format
2003-09-26 paulson 2003-09-26 Conversion of all main protocols from "Shared" to "Public". Removal of Key_supply_ax: modifications to possibility theorems. Improved presentation.
2003-09-23 paulson 2003-09-23 Removal of the Key_supply axiom (affects many possbility proofs) and minor changes
2003-07-24 paulson 2003-07-24 Tidying and replacement of some axioms by specifications
2003-04-26 paulson 2003-04-26 converting more HOL-Auth to new-style theories
2002-08-17 paulson 2002-08-17 tidying of Isar scripts
2001-10-06 wenzelm 2001-10-06 * sane numerals (stage 2): plain "num" syntax (removed "#");
2001-10-05 wenzelm 2001-10-05 sane numerals (stage 1): added generic 1, removed 1' and 2 on nat, "num" syntax (still with "#"), Numeral0, Numeral1;
2001-08-06 paulson 2001-08-06 Changed 1 to 1' (= Suc 0)
2001-02-27 paulson 2001-02-27 Some X-symbols for <notin>, <noteq>, <forall>, <exists> Streamlining of Yahalom proofs Removal of redundant proofs
1998-09-08 paulson 1998-09-08 Got rid of not_Says_to_self and most uses of ~= in definitions and theorems
1998-06-19 paulson 1998-06-19 New example Kerberos_BAN by G Bella