src/HOL/Auth/KerberosIV.thy
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-07-13 paulson 2005-07-13 generlization of some "nat" theorems
2005-06-17 haftmann 2005-06-17 migrated theory headers to new format
2004-06-15 paulson 2004-06-15 slight speed improvement
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-09-04 paulson 2003-09-04 conversion of HOL/Auth/KerberosIV to new-style theory
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
1999-04-20 paulson 1999-04-20 addition of Kerberos IV example