Mercurialisabelle / shortlog
summary | shortlog | changelog | graph | tags | branches | files | gz

 
1996-10-24 paulson 1996-10-24 Two new protocol variants changeset | files
1996-10-24 paulson 1996-10-24 Moved ex_strip_tac to the common part changeset | files
1996-10-24 paulson 1996-10-24 Removal of unused predicate isSpy changeset | files
1996-10-24 paulson 1996-10-24 Handles pathnames in ISABELLECOMP changeset | files
1996-10-21 paulson 1996-10-21 Mentions the possibility of pathnames in ISABELLECOMP; changeset | files
1996-10-21 paulson 1996-10-21 Creates a bigger main window changeset | files
1996-10-21 paulson 1996-10-21 ISABELLECOMP may now have a leading pathname changeset | files
1996-10-21 nipkow 1996-10-21 Used trans_tac (see Provers/nat_transitive.ML) to automate arithmetic. changeset | files
1996-10-21 nipkow 1996-10-21 Added trans_tac (see Provers/nat_transitive.ML) changeset | files
1996-10-21 nipkow 1996-10-21 Solves simple arithmetic goals. changeset | files
1996-10-18 paulson 1996-10-18 Subst as modified by Konrad Slind changeset | files
1996-10-18 paulson 1996-10-18 Konrad Slind's TFL changeset | files
1996-10-18 paulson 1996-10-18 New version of Yahalom, as recommended on p 259 of BAN paper changeset | files
1996-10-18 paulson 1996-10-18 Addition of Reveal message changeset | files
1996-10-18 paulson 1996-10-18 Deleted obsolete rewrites (they are now in HOL/simpdata) changeset | files
1996-10-18 paulson 1996-10-18 Reveal -> Revl changeset | files
1996-10-18 paulson 1996-10-18 The new proof of the lemma for new_nonces_not_seen is faster changeset | files
1996-10-18 paulson 1996-10-18 Generaly tidying up changeset | files
1996-10-18 paulson 1996-10-18 Important correction to comment changeset | files
1996-10-18 paulson 1996-10-18 Replaced excluded_middle_tac by case_tac; tidied proofs changeset | files
1996-10-18 paulson 1996-10-18 Tidied up the proof of A_trust_NS4 changeset | files
1996-10-18 paulson 1996-10-18 Replaced excluded_middle_tac by case_tac changeset | files
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 changeset | files
1996-10-18 paulson 1996-10-18 Now checks that $LISTEN is set changeset | files
1996-10-16 nipkow 1996-10-16 Defined pred using nat_case rather than nat_rec. Added expand_nat_case changeset | files
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) changeset | files
1996-10-15 oheimb 1996-10-15 bound o_apply theorem to thy changeset | files
1996-10-15 paulson 1996-10-15 Removed extraneous spaces from all Makefiles changeset | files
1996-10-15 paulson 1996-10-15 changed prettyprinting of ==> changeset | files
1996-10-15 paulson 1996-10-15 Removed extraneous spaces from all Makefiles changeset | files
1996-10-14 paulson 1996-10-14 Removed call to obsolete totalCPUTimer function changeset | files
1996-10-11 paulson 1996-10-11 Addition of Sequents; removal of Modal and LK changeset | files
1996-10-11 paulson 1996-10-11 Addition of OtwayRees_AN changeset | files
1996-10-10 paulson 1996-10-10 Abadi and Needham's variant of Otway-Rees changeset | files
1996-10-10 paulson 1996-10-10 Deleted obsolete clasets changeset | files
1996-10-10 paulson 1996-10-10 Added comments describing better proofs changeset | files
1996-10-10 paulson 1996-10-10 Simpset removes the de Morgan laws changeset | files
1996-10-10 paulson 1996-10-10 Removed Modal since Sequents contains everything in it changeset | files
1996-10-10 paulson 1996-10-10 Removed LK since Sequents contains everything in it changeset | files
1996-10-10 paulson 1996-10-10 New root file with more description, and merging LK and Modal to Sequents changeset | files
1996-10-10 paulson 1996-10-10 Tidied some proofs: changed needed for de Morgan laws changeset | files
1996-10-10 paulson 1996-10-10 Addition of de Morgan laws changeset | files
1996-10-10 paulson 1996-10-10 Removed Fast_tac made redundant by addition of de Morgan laws changeset | files
1996-10-09 paulson 1996-10-09 Fuller description of examples changeset | files
1996-10-09 paulson 1996-10-09 Plain text README files now redundant due to HTML versions changeset | files
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. changeset | files
1996-10-09 paulson 1996-10-09 Plain text README files now redundant due to HTML versions changeset | files
1996-10-09 paulson 1996-10-09 cond_timeit now catches exception Time, which sml/nj sometimes raised for no obvious reason changeset | files
1996-10-09 paulson 1996-10-09 Updated references changeset | files
1996-10-09 paulson 1996-10-09 Added the de Morgan laws (incl quantifier versions) to basic simpset changeset | files
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) changeset | files
1996-10-08 paulson 1996-10-08 Put in the theorem Says_Crypt_not_lost changeset | files
1996-10-08 paulson 1996-10-08 Put in a simpler and *much* faster proof of no_nonce_OR1_OR2 changeset | files
1996-10-08 paulson 1996-10-08 New guarantees for each line of protocol changeset | files
1996-10-08 paulson 1996-10-08 Addition of Revl rule, and tidying changeset | files
1996-10-08 paulson 1996-10-08 New theorem Crypt_imp_invKey_keysFor changeset | files
1996-10-08 paulson 1996-10-08 Removed command made redundant by the new one-point rules changeset | files
1996-10-08 paulson 1996-10-08 Introduction of Slow_tac and Slow_best_tac changeset | files
1996-10-08 paulson 1996-10-08 Addition of one-point quantifier rewrite rules changeset | files
1996-10-07 paulson 1996-10-07 Simple tidying changeset | files
isabelle