src/HOL/Auth/Message.ML
1996-12-16 paulson 1996-12-16 New tactic: prove_unique_tac
1996-12-13 paulson 1996-12-13 Addition of the Hash constructor Strengthening spy_analz_tac
1996-12-05 paulson 1996-12-05 Moved much common material to Message.ML
1996-11-29 paulson 1996-11-29 Swapped arguments of Crypt (for clarity and because it is conventional)
1996-11-08 paulson 1996-11-08 Ran expandshort
1996-11-01 paulson 1996-11-01 New, purely illustrative result Crypt_synth_analz
1996-10-18 paulson 1996-10-18 Replaced excluded_middle_tac by case_tac
1996-10-08 paulson 1996-10-08 New theorem Crypt_imp_invKey_keysFor
1996-10-07 paulson 1996-10-07 New theorem Crypt_Fake_parts_insert
1996-09-26 paulson 1996-09-26 Introduction of "lost" argument Changed Enemy -> Spy Ran expandshort
1996-09-26 paulson 1996-09-26 Last working version prior to addition of "lost" component
1996-09-25 paulson 1996-09-25 Last working version prior to introduction of "lost"
1996-09-23 paulson 1996-09-23 New laws for messages
1996-09-13 paulson 1996-09-13 Reordering of premises for cut theorems, and new law MPair_synth_analz
1996-09-13 paulson 1996-09-13 Removal of obsolete thm Fake_parts_insert
1996-09-09 paulson 1996-09-09 Stronger proofs; work for Otway-Rees
1996-09-03 paulson 1996-09-03 New theorems for Fake case
1996-08-20 paulson 1996-08-20 Working version of NS, messages 1-3, WITH INTERLEAVING
1996-08-19 paulson 1996-08-19 Renaming of functions, and tidying
1996-07-29 paulson 1996-07-29 Works up to main theorem, then XXX...X
1996-07-26 paulson 1996-07-26 Auth proofs work up to the XXX...
1996-07-11 paulson 1996-07-11 Added Msg 3; works up to Says_Server_imp_Key_newK
1996-06-28 paulson 1996-06-28 Proving safety properties of authentication protocols