1996-10-24 paulson 1996-10-24 Two new protocol variants
1996-10-24 paulson 1996-10-24 Moved ex_strip_tac to the common part
1996-10-24 paulson 1996-10-24 Removal of unused predicate isSpy
1996-10-24 paulson 1996-10-24 Handles pathnames in ISABELLECOMP
1996-10-21 paulson 1996-10-21 Mentions the possibility of pathnames in ISABELLECOMP;
1996-10-21 paulson 1996-10-21 Creates a bigger main window
1996-10-21 paulson 1996-10-21 ISABELLECOMP may now have a leading pathname
1996-10-21 nipkow 1996-10-21 Used trans_tac (see Provers/nat_transitive.ML) to automate arithmetic.
1996-10-21 nipkow 1996-10-21 Added trans_tac (see Provers/nat_transitive.ML)
1996-10-21 nipkow 1996-10-21 Solves simple arithmetic goals.
1996-10-18 paulson 1996-10-18 Subst as modified by Konrad Slind
1996-10-18 paulson 1996-10-18 Konrad Slind's TFL
1996-10-18 paulson 1996-10-18 New version of Yahalom, as recommended on p 259 of BAN paper
1996-10-18 paulson 1996-10-18 Addition of Reveal message
1996-10-18 paulson 1996-10-18 Deleted obsolete rewrites (they are now in HOL/simpdata)
1996-10-18 paulson 1996-10-18 Reveal -> Revl
1996-10-18 paulson 1996-10-18 The new proof of the lemma for new_nonces_not_seen is faster
1996-10-18 paulson 1996-10-18 Generaly tidying up
1996-10-18 paulson 1996-10-18 Important correction to comment
1996-10-18 paulson 1996-10-18 Replaced excluded_middle_tac by case_tac; tidied proofs
1996-10-18 paulson 1996-10-18 Tidied up the proof of A_trust_NS4
1996-10-18 paulson 1996-10-18 Replaced excluded_middle_tac by case_tac
1996-10-18 paulson 1996-10-18 Moving the CPUtimer declaration into cond_timeit should prevent the problems that caused exn TIME to be raised
1996-10-18 paulson 1996-10-18 Now checks that $LISTEN is set
1996-10-16 nipkow 1996-10-16 Defined pred using nat_case rather than nat_rec. Added expand_nat_case
1996-10-15 oheimb 1996-10-15 corrected `correction` of o_assoc (of version 1.14), (this change has actually been done in the previous commit 1.25)
1996-10-15 oheimb 1996-10-15 bound o_apply theorem to thy
1996-10-15 paulson 1996-10-15 Removed extraneous spaces from all Makefiles
1996-10-15 paulson 1996-10-15 changed prettyprinting of ==>
1996-10-15 paulson 1996-10-15 Removed extraneous spaces from all Makefiles
1996-10-14 paulson 1996-10-14 Removed call to obsolete totalCPUTimer function
1996-10-11 paulson 1996-10-11 Addition of Sequents; removal of Modal and LK
1996-10-11 paulson 1996-10-11 Addition of OtwayRees_AN
1996-10-10 paulson 1996-10-10 Abadi and Needham's variant of Otway-Rees
1996-10-10 paulson 1996-10-10 Deleted obsolete clasets
1996-10-10 paulson 1996-10-10 Added comments describing better proofs
1996-10-10 paulson 1996-10-10 Simpset removes the de Morgan laws
1996-10-10 paulson 1996-10-10 Removed Modal since Sequents contains everything in it
1996-10-10 paulson 1996-10-10 Removed LK since Sequents contains everything in it
1996-10-10 paulson 1996-10-10 New root file with more description, and merging LK and Modal to Sequents
1996-10-10 paulson 1996-10-10 Tidied some proofs: changed needed for de Morgan laws
1996-10-10 paulson 1996-10-10 Addition of de Morgan laws
1996-10-10 paulson 1996-10-10 Removed Fast_tac made redundant by addition of de Morgan laws
1996-10-09 paulson 1996-10-09 Fuller description of examples
1996-10-09 paulson 1996-10-09 Plain text README files now redundant due to HTML versions
1996-10-09 paulson 1996-10-09 New version of axiom sees1_Says: Previously it only allowed the SENDER to see the content of messages... Now instead the RECIPIENT sees the messages. This change had no effect on subsequent proofs because protocol rules refer specifically to the relevant messages sent to an agent.
1996-10-09 paulson 1996-10-09 Plain text README files now redundant due to HTML versions
1996-10-09 paulson 1996-10-09 cond_timeit now catches exception Time, which sml/nj sometimes raised for no obvious reason
1996-10-09 paulson 1996-10-09 Updated references
1996-10-09 paulson 1996-10-09 Added the de Morgan laws (incl quantifier versions) to basic simpset
1996-10-09 paulson 1996-10-09 New unified treatment of sequent calculi by Sara Kalvala combines the old LK and Modal with the new ILL (Int. Linear Logic)
1996-10-08 paulson 1996-10-08 Put in the theorem Says_Crypt_not_lost
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