1996-10-08 paulson 1996-10-08 Put in a simpler and *much* faster proof of no_nonce_OR1_OR2
1996-10-08 paulson 1996-10-08 New guarantees for each line of protocol
1996-10-08 paulson 1996-10-08 Addition of Revl rule, and tidying
1996-10-08 paulson 1996-10-08 New theorem Crypt_imp_invKey_keysFor
1996-10-08 paulson 1996-10-08 Removed command made redundant by the new one-point rules
1996-10-08 paulson 1996-10-08 Introduction of Slow_tac and Slow_best_tac
1996-10-08 paulson 1996-10-08 Addition of one-point quantifier rewrite rules
1996-10-07 paulson 1996-10-07 Simple tidying
1996-10-07 paulson 1996-10-07 New proof required by change to simpdata.ML
1996-10-07 paulson 1996-10-07 Now replaces shorthand commands even if indented
1996-10-07 paulson 1996-10-07 New theorem Crypt_Fake_parts_insert
1996-10-07 paulson 1996-10-07 Simplified a proof
1996-10-07 paulson 1996-10-07 New comment in header
1996-10-07 paulson 1996-10-07 Tidied up some proofs
1996-10-07 paulson 1996-10-07 Ran expandshort
1996-10-07 paulson 1996-10-07 Removed commands made redundant by new one-point rules
1996-10-07 paulson 1996-10-07 Ran expandshort
1996-10-07 paulson 1996-10-07 New one-point rules for quantifiers
1996-10-01 paulson 1996-10-01 Greatly simplified the proof of A_can_trust
1996-10-01 paulson 1996-10-01 Working again with new theory Shared
1996-10-01 paulson 1996-10-01 Simplified main theorem by abstracting out newK
1996-10-01 paulson 1996-10-01 Moved sees_lost_agent_subset_sees_Spy to common file, and simplified main thm
1996-10-01 paulson 1996-10-01 Moved sees_lost_agent_subset_sees_Spy to common file
1996-10-01 paulson 1996-10-01 Added new guarantees for A and B
1996-10-01 wenzelm 1996-10-01 added shyps comment;
1996-09-30 nipkow 1996-09-30 Inserted check for rewrite rules which introduce extra Vars on the rhs.
1996-09-30 paulson 1996-09-30 Removed some dead wood. Transferred lemmas used to prove analz_image_newK to Shared.ML
1996-09-30 paulson 1996-09-30 Improved discussion of shyps thanks to Markus Wenzel
1996-09-30 paulson 1996-09-30 prune_params_tac no longer rewrites main goal
1996-09-26 paulson 1996-09-26 Added catch-all clause to drop, preventing exception Match
1996-09-26 paulson 1996-09-26 Now replaces uses of ssubst by stac
1996-09-26 paulson 1996-09-26 Documented sort hypotheses and improved discussion of derivations
1996-09-26 paulson 1996-09-26 Documented defer_tac and moved back the obsolete tactics like fold_tac
1996-09-26 paulson 1996-09-26 Documented stac, and updated the documentation of hyp_subst_tac
1996-09-26 paulson 1996-09-26 Declared stac
1996-09-26 paulson 1996-09-26 Ran expandshort; used stac instead of ssubst
1996-09-26 paulson 1996-09-26 Ran expandshort; used stac instead of ssubst
1996-09-26 paulson 1996-09-26 Ran expandshort; used stac instead of ssubst
1996-09-26 paulson 1996-09-26 Ran expandshort; used stac instead of ssubst
1996-09-26 paulson 1996-09-26 Introduction of "lost" argument Changed Enemy -> Spy Ran expandshort
1996-09-26 paulson 1996-09-26 Ran expandshort
1996-09-26 paulson 1996-09-26 Changed freeze to freeze_thaw
1996-09-26 paulson 1996-09-26 Generalized freeze to freeze_thaw in order to implement defer_tac
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 before "lost"
1996-09-25 paulson 1996-09-25 Last working version prior to introduction of "lost"
1996-09-25 paulson 1996-09-25 Prevention of Overflow exception (for SML/NJ) in gensym
1996-09-25 paulson 1996-09-25 Rationalized the rewriting of membership for {} and insert by deleting the redundant theorems in_empty and in_insert
1996-09-25 paulson 1996-09-25 Calls discgarb -c to realize dramatic space savings!
1996-09-24 paulson 1996-09-24 Fixed spelling error in comment
1996-09-24 paulson 1996-09-24 Added miniscoping for UN and INT
1996-09-24 paulson 1996-09-24 Restoration of reference to Nipkow, LICS, 1993
1996-09-24 nipkow 1996-09-24 Moved Option out of IOA into core HOL
1996-09-24 nipkow 1996-09-24 Moved Option into core HOL which caused a few local changes.
1996-09-23 paulson 1996-09-23 Proofs made more robust to work in presence of le_refl
1996-09-23 paulson 1996-09-23 Now uses init_html
1996-09-23 paulson 1996-09-23 Simplification of proof of unique_session_keys
1996-09-23 paulson 1996-09-23 Correction of protocol; addition of Reveal message; proofs of correctness in its presence
1996-09-23 paulson 1996-09-23 Proof of Says_imp_old_keys is now more robust
1996-09-23 paulson 1996-09-23 Removal of the Notes constructor