src/HOL/Auth/Message.thy
1999-07-21 paulson 1999-07-21 tweaked proofs to handle new freeness reasoning for data c onstructors
1999-06-10 paulson 1999-06-10 new translation to allow images over Nonce
1998-10-16 paulson 1998-10-16 parent is Main
1998-08-03 paulson 1998-08-03 Better comments
1998-07-24 berghofe 1998-07-24 Adapted to new datatype package.
1998-06-30 berghofe 1998-06-30 Adapted to new inductive definition package.
1997-09-11 paulson 1997-09-11 Split base cases from "msg" to "atomic" in order to reduce the number of freeness theorems
1997-01-17 paulson 1997-01-17 Now with Andy Gordon's treatment of freshness to replace newN/K
1997-01-07 paulson 1997-01-07 Incorporation of HPair into Message
1996-12-13 paulson 1996-12-13 Addition of the Hash constructor Strengthening spy_analz_tac
1996-11-29 paulson 1996-11-29 Swapped arguments of Crypt (for clarity and because it is conventional)
1996-10-24 paulson 1996-10-24 Removal of unused predicate isSpy
1996-09-26 paulson 1996-09-26 Introduction of "lost" argument Changed Enemy -> Spy Ran expandshort
1996-09-23 paulson 1996-09-23 Simplification of definition of synth
1996-09-03 paulson 1996-09-03 Fixed pretty-printing of {|...|}
1996-08-19 paulson 1996-08-19 Renaming of functions, and tidying
1996-06-28 paulson 1996-06-28 Proving safety properties of authentication protocols