Tue, 15 Oct 1996 16:40:04 +0200 corrected `correction` of o_assoc (of version 1.14),
oheimb [Tue, 15 Oct 1996 16:40:04 +0200] rev 2098
corrected `correction` of o_assoc (of version 1.14), (this change has actually been done in the previous commit 1.25)
Tue, 15 Oct 1996 16:32:59 +0200 bound o_apply theorem to thy
oheimb [Tue, 15 Oct 1996 16:32:59 +0200] rev 2097
bound o_apply theorem to thy
Tue, 15 Oct 1996 10:58:59 +0200 Removed extraneous spaces from all Makefiles
paulson [Tue, 15 Oct 1996 10:58:59 +0200] rev 2096
Removed extraneous spaces from all Makefiles
Tue, 15 Oct 1996 10:55:57 +0200 changed prettyprinting of ==>
paulson [Tue, 15 Oct 1996 10:55:57 +0200] rev 2095
changed prettyprinting of ==>
Tue, 15 Oct 1996 10:46:42 +0200 Removed extraneous spaces from all Makefiles
paulson [Tue, 15 Oct 1996 10:46:42 +0200] rev 2094
Removed extraneous spaces from all Makefiles
Mon, 14 Oct 1996 11:08:54 +0200 Removed call to obsolete totalCPUTimer function
paulson [Mon, 14 Oct 1996 11:08:54 +0200] rev 2093
Removed call to obsolete totalCPUTimer function
Fri, 11 Oct 1996 10:55:03 +0200 Addition of Sequents; removal of Modal and LK
paulson [Fri, 11 Oct 1996 10:55:03 +0200] rev 2092
Addition of Sequents; removal of Modal and LK
Fri, 11 Oct 1996 10:52:54 +0200 Addition of OtwayRees_AN
paulson [Fri, 11 Oct 1996 10:52:54 +0200] rev 2091
Addition of OtwayRees_AN
Thu, 10 Oct 1996 18:40:34 +0200 Abadi and Needham's variant of Otway-Rees
paulson [Thu, 10 Oct 1996 18:40:34 +0200] rev 2090
Abadi and Needham's variant of Otway-Rees
Thu, 10 Oct 1996 12:00:23 +0200 Deleted obsolete clasets
paulson [Thu, 10 Oct 1996 12:00:23 +0200] rev 2089
Deleted obsolete clasets
Thu, 10 Oct 1996 11:59:01 +0200 Added comments describing better proofs
paulson [Thu, 10 Oct 1996 11:59:01 +0200] rev 2088
Added comments describing better proofs
Thu, 10 Oct 1996 11:58:40 +0200 Simpset removes the de Morgan laws
paulson [Thu, 10 Oct 1996 11:58:40 +0200] rev 2087
Simpset removes the de Morgan laws
Thu, 10 Oct 1996 11:13:48 +0200 Removed Modal since Sequents contains everything in it
paulson [Thu, 10 Oct 1996 11:13:48 +0200] rev 2086
Removed Modal since Sequents contains everything in it
Thu, 10 Oct 1996 11:09:03 +0200 Removed LK since Sequents contains everything in it
paulson [Thu, 10 Oct 1996 11:09:03 +0200] rev 2085
Removed LK since Sequents contains everything in it
Thu, 10 Oct 1996 10:57:33 +0200 New root file with more description, and merging LK and Modal to Sequents
paulson [Thu, 10 Oct 1996 10:57:33 +0200] rev 2084
New root file with more description, and merging LK and Modal to Sequents
Thu, 10 Oct 1996 10:47:26 +0200 Tidied some proofs: changed needed for de Morgan laws
paulson [Thu, 10 Oct 1996 10:47:26 +0200] rev 2083
Tidied some proofs: changed needed for de Morgan laws
Thu, 10 Oct 1996 10:46:14 +0200 Addition of de Morgan laws
paulson [Thu, 10 Oct 1996 10:46:14 +0200] rev 2082
Addition of de Morgan laws
Thu, 10 Oct 1996 10:45:20 +0200 Removed Fast_tac made redundant by addition of de Morgan laws
paulson [Thu, 10 Oct 1996 10:45:20 +0200] rev 2081
Removed Fast_tac made redundant by addition of de Morgan laws
Wed, 09 Oct 1996 13:50:28 +0200 Fuller description of examples
paulson [Wed, 09 Oct 1996 13:50:28 +0200] rev 2080
Fuller description of examples
Wed, 09 Oct 1996 13:47:38 +0200 Plain text README files now redundant due to HTML versions
paulson [Wed, 09 Oct 1996 13:47:38 +0200] rev 2079
Plain text README files now redundant due to HTML versions
Wed, 09 Oct 1996 13:43:51 +0200 New version of axiom sees1_Says:
paulson [Wed, 09 Oct 1996 13:43:51 +0200] rev 2078
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.
Wed, 09 Oct 1996 13:39:25 +0200 Plain text README files now redundant due to HTML versions
paulson [Wed, 09 Oct 1996 13:39:25 +0200] rev 2077
Plain text README files now redundant due to HTML versions
Wed, 09 Oct 1996 13:38:11 +0200 cond_timeit now catches exception Time, which sml/nj
paulson [Wed, 09 Oct 1996 13:38:11 +0200] rev 2076
cond_timeit now catches exception Time, which sml/nj sometimes raised for no obvious reason
Wed, 09 Oct 1996 13:37:00 +0200 Updated references
paulson [Wed, 09 Oct 1996 13:37:00 +0200] rev 2075
Updated references
Wed, 09 Oct 1996 13:36:17 +0200 Added the de Morgan laws (incl quantifier versions) to basic simpset
paulson [Wed, 09 Oct 1996 13:36:17 +0200] rev 2074
Added the de Morgan laws (incl quantifier versions) to basic simpset
Wed, 09 Oct 1996 13:32:33 +0200 New unified treatment of sequent calculi by Sara Kalvala
paulson [Wed, 09 Oct 1996 13:32:33 +0200] rev 2073
New unified treatment of sequent calculi by Sara Kalvala combines the old LK and Modal with the new ILL (Int. Linear Logic)
Tue, 08 Oct 1996 10:28:02 +0200 Put in the theorem Says_Crypt_not_lost
paulson [Tue, 08 Oct 1996 10:28:02 +0200] rev 2072
Put in the theorem Says_Crypt_not_lost
Tue, 08 Oct 1996 10:27:31 +0200 Put in a simpler and *much* faster proof of no_nonce_OR1_OR2
paulson [Tue, 08 Oct 1996 10:27:31 +0200] rev 2071
Put in a simpler and *much* faster proof of no_nonce_OR1_OR2
Tue, 08 Oct 1996 10:26:23 +0200 New guarantees for each line of protocol
paulson [Tue, 08 Oct 1996 10:26:23 +0200] rev 2070
New guarantees for each line of protocol
Tue, 08 Oct 1996 10:21:04 +0200 Addition of Revl rule, and tidying
paulson [Tue, 08 Oct 1996 10:21:04 +0200] rev 2069
Addition of Revl rule, and tidying
(0) -1000 -300 -100 -50 -30 +30 +50 +100 +300 +1000 +3000 +10000 +30000 tip