paulson [Thu, 10 Oct 1996 10:45:20 +0200] rev 2081
Removed Fast_tac made redundant by addition of de Morgan laws
paulson [Wed, 09 Oct 1996 13:50:28 +0200] rev 2080
Fuller description of examples
paulson [Wed, 09 Oct 1996 13:47:38 +0200] rev 2079
Plain text README files now redundant due to HTML versions
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.
paulson [Wed, 09 Oct 1996 13:39:25 +0200] rev 2077
Plain text README files now redundant due to HTML versions
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
paulson [Wed, 09 Oct 1996 13:37:00 +0200] rev 2075
Updated references
paulson [Wed, 09 Oct 1996 13:36:17 +0200] rev 2074
Added the de Morgan laws (incl quantifier versions) to basic simpset
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)
paulson [Tue, 08 Oct 1996 10:28:02 +0200] rev 2072
Put in the theorem Says_Crypt_not_lost
paulson [Tue, 08 Oct 1996 10:27:31 +0200] rev 2071
Put in a simpler and *much* faster proof of no_nonce_OR1_OR2
paulson [Tue, 08 Oct 1996 10:26:23 +0200] rev 2070
New guarantees for each line of protocol
paulson [Tue, 08 Oct 1996 10:21:04 +0200] rev 2069
Addition of Revl rule, and tidying
paulson [Tue, 08 Oct 1996 10:19:31 +0200] rev 2068
New theorem Crypt_imp_invKey_keysFor
paulson [Tue, 08 Oct 1996 10:18:53 +0200] rev 2067
Removed command made redundant by the new one-point rules
paulson [Tue, 08 Oct 1996 10:18:18 +0200] rev 2066
Introduction of Slow_tac and Slow_best_tac
paulson [Tue, 08 Oct 1996 10:17:50 +0200] rev 2065
Addition of one-point quantifier rewrite rules
paulson [Mon, 07 Oct 1996 10:55:51 +0200] rev 2064
Simple tidying
paulson [Mon, 07 Oct 1996 10:47:01 +0200] rev 2063
New proof required by change to simpdata.ML
paulson [Mon, 07 Oct 1996 10:43:40 +0200] rev 2062
Now replaces shorthand commands even if indented
paulson [Mon, 07 Oct 1996 10:41:26 +0200] rev 2061
New theorem Crypt_Fake_parts_insert
paulson [Mon, 07 Oct 1996 10:40:51 +0200] rev 2060
Simplified a proof
paulson [Mon, 07 Oct 1996 10:35:47 +0200] rev 2059
New comment in header
paulson [Mon, 07 Oct 1996 10:34:58 +0200] rev 2058
Tidied up some proofs
paulson [Mon, 07 Oct 1996 10:31:50 +0200] rev 2057
Ran expandshort
paulson [Mon, 07 Oct 1996 10:28:44 +0200] rev 2056
Removed commands made redundant by new one-point rules
paulson [Mon, 07 Oct 1996 10:26:00 +0200] rev 2055
Ran expandshort
paulson [Mon, 07 Oct 1996 10:23:35 +0200] rev 2054
New one-point rules for quantifiers
paulson [Tue, 01 Oct 1996 18:19:12 +0200] rev 2053
Greatly simplified the proof of A_can_trust
paulson [Tue, 01 Oct 1996 18:10:33 +0200] rev 2052
Working again with new theory Shared