src/HOL/Auth/NS_Public.thy
2010-07-22 wenzelm updated some headers;
2009-10-17 wenzelm eliminated hard tabulators, guessing at each author's individual tab-width;
2007-07-11 berghofe Adapted to new inductive definition package.
2005-06-17 haftmann migrated theory headers to new format
2003-09-26 paulson Conversion of all main protocols from "Shared" to "Public".
2003-09-23 paulson Removal of the Key_supply axiom (affects many possbility proofs) and minor
2003-05-05 paulson improved presentation of HOL/Auth theories
2003-04-26 paulson converting more HOL-Auth to new-style theories
2003-04-25 paulson Changes required by the certified email protocol
2002-08-17 paulson tidying of Isar scripts
2001-06-09 paulson renaming of evs in the Fake rule
2001-03-29 paulson misc tidying; changing the predicate isSymKey to the set symKeys
2001-02-13 paulson partial conversion to Isar script style
1998-09-08 paulson Got rid of not_Says_to_self and most uses of ~= in definitions and theorems
1997-09-18 paulson Global change: lost->bad and sees Spy->spies
1997-09-05 paulson Renamed "evs" to "evs1", "evs2", etc. in protocol inductive definition
1997-07-22 paulson Deleted the superfluous assumption A ~= B, which must hold anyway by induction
1997-07-14 paulson Changing "lost" from a parameter of protocol definitions to a constant.
1997-06-27 paulson Corrected indentations and margins after the renaming of "set_of_list"
1997-06-26 nipkow set_of_list -> set
1997-01-23 paulson Cosmetic improvements
1997-01-23 paulson Mended spelling error
1997-01-17 paulson Now with Andy Gordon's treatment of freshness to replace newN/K
1997-01-09 paulson New treatment of nonce creation
1996-12-19 paulson Extensive tidying and simplification, largely stemming from
1996-12-05 paulson Public-key examples
less more (0) tip