paulson [Fri, 01 Nov 1996 15:25:21 +0100] rev 2144
Replaced foldl nodup_TVars by nodup_TVars_list -- for a big speedup on Poly/ML
paulson [Fri, 01 Nov 1996 15:15:39 +0100] rev 2143
Replaced min by Int.min
paulson [Fri, 01 Nov 1996 15:14:25 +0100] rev 2142
Deleted Olist constructor. Replaced minidx by "above" function
paulson [Fri, 01 Nov 1996 15:12:21 +0100] rev 2141
Now defines structure Int
paulson [Wed, 30 Oct 1996 11:21:24 +0100] rev 2140
Changed some mem calls to mem_int for greater efficiency (not that it could matter)
paulson [Wed, 30 Oct 1996 11:20:27 +0100] rev 2139
Only calls nodup_Vars if really necessary. We get a speedup of nearly 6%
paulson [Wed, 30 Oct 1996 11:19:09 +0100] rev 2138
Changed some mem calls to mem_string for greater efficiency (not that it could matter)
paulson [Wed, 30 Oct 1996 11:17:54 +0100] rev 2137
Minor updates
paulson [Wed, 30 Oct 1996 11:15:09 +0100] rev 2136
Updated references
paulson [Mon, 28 Oct 1996 15:59:39 +0100] rev 2135
Minor corrections
nipkow [Mon, 28 Oct 1996 15:36:18 +0100] rev 2134
Renamed and shuffled a few thms.
paulson [Mon, 28 Oct 1996 13:02:37 +0100] rev 2133
Simplified proofs
paulson [Mon, 28 Oct 1996 13:01:25 +0100] rev 2132
Tidied up a big mess in UN_parts_sees_Says
paulson [Mon, 28 Oct 1996 12:55:24 +0100] rev 2131
Changing from the Reveal to the Oops rule
nipkow [Sun, 27 Oct 1996 13:47:02 +0100] rev 2130
Simplifid proofs.
nipkow [Fri, 25 Oct 1996 15:02:09 +0200] rev 2129
Added (? x. t=x) = True
paulson [Thu, 24 Oct 1996 11:41:43 +0200] rev 2128
Documents the use of negative arguments to choplev and prlev
paulson [Thu, 24 Oct 1996 10:43:38 +0200] rev 2127
Changed comment to illustrate use of pathname
paulson [Thu, 24 Oct 1996 10:42:42 +0200] rev 2126
Allowing negative levels (as offsets) in prlev and choplev
paulson [Thu, 24 Oct 1996 10:38:35 +0200] rev 2125
New Oops message, with Server as source to ensure
correct nonces
paulson [Thu, 24 Oct 1996 10:36:29 +0200] rev 2124
New theorem Crypt_Spy_analz_lost; improvements to spy_analz_tac; ex_strip_tac
paulson [Thu, 24 Oct 1996 10:33:27 +0200] rev 2123
Two new protocol variants
paulson [Thu, 24 Oct 1996 10:31:17 +0200] rev 2122
Moved ex_strip_tac to the common part
paulson [Thu, 24 Oct 1996 10:30:43 +0200] rev 2121
Removal of unused predicate isSpy
paulson [Thu, 24 Oct 1996 10:30:17 +0200] rev 2120
Handles pathnames in ISABELLECOMP
paulson [Mon, 21 Oct 1996 11:37:21 +0200] rev 2119
Mentions the possibility of pathnames in ISABELLECOMP;
paulson [Mon, 21 Oct 1996 11:36:57 +0200] rev 2118
Creates a bigger main window
paulson [Mon, 21 Oct 1996 11:18:34 +0200] rev 2117
ISABELLECOMP may now have a leading pathname
nipkow [Mon, 21 Oct 1996 09:51:18 +0200] rev 2116
Used trans_tac (see Provers/nat_transitive.ML) to automate arithmetic.
nipkow [Mon, 21 Oct 1996 09:50:50 +0200] rev 2115
Added trans_tac (see Provers/nat_transitive.ML)
nipkow [Mon, 21 Oct 1996 09:49:41 +0200] rev 2114
Solves simple arithmetic goals.
paulson [Fri, 18 Oct 1996 12:54:19 +0200] rev 2113
Subst as modified by Konrad Slind
paulson [Fri, 18 Oct 1996 12:41:04 +0200] rev 2112
Konrad Slind's TFL
paulson [Fri, 18 Oct 1996 11:43:14 +0200] rev 2111
New version of Yahalom, as recommended on p 259 of BAN paper
paulson [Fri, 18 Oct 1996 11:42:41 +0200] rev 2110
Addition of Reveal message
paulson [Fri, 18 Oct 1996 11:42:17 +0200] rev 2109
Deleted obsolete rewrites (they are now in HOL/simpdata)
paulson [Fri, 18 Oct 1996 11:41:41 +0200] rev 2108
Reveal -> Revl
paulson [Fri, 18 Oct 1996 11:41:04 +0200] rev 2107
The new proof of the lemma for new_nonces_not_seen is faster
paulson [Fri, 18 Oct 1996 11:39:55 +0200] rev 2106
Generaly tidying up
paulson [Fri, 18 Oct 1996 11:39:10 +0200] rev 2105
Important correction to comment
paulson [Fri, 18 Oct 1996 11:38:17 +0200] rev 2104
Replaced excluded_middle_tac by case_tac; tidied proofs
paulson [Fri, 18 Oct 1996 11:37:19 +0200] rev 2103
Tidied up the proof of A_trust_NS4
paulson [Fri, 18 Oct 1996 11:33:02 +0200] rev 2102
Replaced excluded_middle_tac by case_tac
paulson [Fri, 18 Oct 1996 11:32:38 +0200] rev 2101
Moving the CPUtimer declaration into cond_timeit should
prevent the problems that caused exn TIME to be raised
paulson [Fri, 18 Oct 1996 11:31:33 +0200] rev 2100
Now checks that $LISTEN is set
nipkow [Wed, 16 Oct 1996 10:37:17 +0200] rev 2099
Defined pred using nat_case rather than nat_rec.
Added expand_nat_case
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)
oheimb [Tue, 15 Oct 1996 16:32:59 +0200] rev 2097
bound o_apply theorem to thy
paulson [Tue, 15 Oct 1996 10:58:59 +0200] rev 2096
Removed extraneous spaces from all Makefiles
paulson [Tue, 15 Oct 1996 10:55:57 +0200] rev 2095
changed prettyprinting of ==>
paulson [Tue, 15 Oct 1996 10:46:42 +0200] rev 2094
Removed extraneous spaces from all Makefiles
paulson [Mon, 14 Oct 1996 11:08:54 +0200] rev 2093
Removed call to obsolete totalCPUTimer function
paulson [Fri, 11 Oct 1996 10:55:03 +0200] rev 2092
Addition of Sequents; removal of Modal and LK
paulson [Fri, 11 Oct 1996 10:52:54 +0200] rev 2091
Addition of OtwayRees_AN
paulson [Thu, 10 Oct 1996 18:40:34 +0200] rev 2090
Abadi and Needham's variant of Otway-Rees
paulson [Thu, 10 Oct 1996 12:00:23 +0200] rev 2089
Deleted obsolete clasets
paulson [Thu, 10 Oct 1996 11:59:01 +0200] rev 2088
Added comments describing better proofs
paulson [Thu, 10 Oct 1996 11:58:40 +0200] rev 2087
Simpset removes the de Morgan laws
paulson [Thu, 10 Oct 1996 11:13:48 +0200] rev 2086
Removed Modal 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
paulson [Thu, 10 Oct 1996 10:57:33 +0200] rev 2084
New root file with more description, and merging LK and Modal to Sequents
paulson [Thu, 10 Oct 1996 10:47:26 +0200] rev 2083
Tidied some proofs: changed needed for de Morgan laws
paulson [Thu, 10 Oct 1996 10:46:14 +0200] rev 2082
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
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
paulson [Tue, 01 Oct 1996 17:44:54 +0200] rev 2051
Simplified main theorem by abstracting out newK
paulson [Tue, 01 Oct 1996 17:07:41 +0200] rev 2050
Moved sees_lost_agent_subset_sees_Spy to common file, and simplified main thm
paulson [Tue, 01 Oct 1996 15:58:29 +0200] rev 2049
Moved sees_lost_agent_subset_sees_Spy to common file