src/HOL/Auth/Yahalom.ML
1996-09-30 paulson 1996-09-30 Removed some dead wood. Transferred lemmas used to prove analz_image_newK to Shared.ML
1996-09-26 paulson 1996-09-26 Introduction of "lost" argument Changed Enemy -> Spy Ran expandshort
1996-09-25 paulson 1996-09-25 Last working version prior to introduction of "lost"
1996-09-23 paulson 1996-09-23 Proof of Says_imp_old_keys is now more robust
1996-09-13 paulson 1996-09-13 Reformatting; proved B_gets_secure_key
1996-09-13 paulson 1996-09-13 Addition of Yahalom protocol
1996-09-12 paulson 1996-09-12 Tidied many proofs, using AddIffs to let equivalences take the place of separate Intr and Elim rules. Also deleted most named clasets.