src/HOL/Auth/OtwayRees.ML
1996-10-28 nipkow 1996-10-28 Renamed and shuffled a few thms.
1996-10-18 paulson 1996-10-18 Replaced excluded_middle_tac by case_tac; tidied proofs
1996-10-08 paulson 1996-10-08 Put in a simpler and *much* faster proof of no_nonce_OR1_OR2
1996-10-07 paulson 1996-10-07 Simple tidying
1996-10-01 paulson 1996-10-01 Greatly simplified the proof of A_can_trust
1996-10-01 paulson 1996-10-01 Added new guarantees for A and B
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 Correction of protocol; addition of Reveal message; proofs of correctness in its presence
1996-09-13 paulson 1996-09-13 Reformatting
1996-09-13 paulson 1996-09-13 Uses the improved enemy_analz_tac of Shared.ML, with simpler proofs Weak liveness
1996-09-09 paulson 1996-09-09 "bad" set simplifies statements of many theorems
1996-09-09 paulson 1996-09-09 Stronger proofs; work for Otway-Rees
1996-09-03 paulson 1996-09-03 A further tidying
1996-09-03 paulson 1996-09-03 Initial working proof of Otway-Rees protocol