Mon, 28 Oct 1996 15:36:18 +0100 nipkow Renamed and shuffled a few thms.
Mon, 28 Oct 1996 13:02:37 +0100 paulson Simplified proofs
Mon, 28 Oct 1996 13:01:25 +0100 paulson Tidied up a big mess in UN_parts_sees_Says
Mon, 28 Oct 1996 12:55:24 +0100 paulson Changing from the Reveal to the Oops rule
Sun, 27 Oct 1996 13:47:02 +0100 nipkow Simplifid proofs.
Fri, 25 Oct 1996 15:02:09 +0200 nipkow Added (? x. t=x) = True
Thu, 24 Oct 1996 11:41:43 +0200 paulson Documents the use of negative arguments to choplev and prlev
Thu, 24 Oct 1996 10:43:38 +0200 paulson Changed comment to illustrate use of pathname
Thu, 24 Oct 1996 10:42:42 +0200 paulson Allowing negative levels (as offsets) in prlev and choplev
Thu, 24 Oct 1996 10:38:35 +0200 paulson New Oops message, with Server as source to ensure
Thu, 24 Oct 1996 10:36:29 +0200 paulson New theorem Crypt_Spy_analz_lost; improvements to spy_analz_tac; ex_strip_tac
Thu, 24 Oct 1996 10:33:27 +0200 paulson Two new protocol variants
Thu, 24 Oct 1996 10:31:17 +0200 paulson Moved ex_strip_tac to the common part
Thu, 24 Oct 1996 10:30:43 +0200 paulson Removal of unused predicate isSpy
Thu, 24 Oct 1996 10:30:17 +0200 paulson Handles pathnames in ISABELLECOMP
Mon, 21 Oct 1996 11:37:21 +0200 paulson Mentions the possibility of pathnames in ISABELLECOMP;
Mon, 21 Oct 1996 11:36:57 +0200 paulson Creates a bigger main window
Mon, 21 Oct 1996 11:18:34 +0200 paulson ISABELLECOMP may now have a leading pathname
Mon, 21 Oct 1996 09:51:18 +0200 nipkow Used trans_tac (see Provers/nat_transitive.ML) to automate arithmetic.
Mon, 21 Oct 1996 09:50:50 +0200 nipkow Added trans_tac (see Provers/nat_transitive.ML)
Mon, 21 Oct 1996 09:49:41 +0200 nipkow Solves simple arithmetic goals.
Fri, 18 Oct 1996 12:54:19 +0200 paulson Subst as modified by Konrad Slind
Fri, 18 Oct 1996 12:41:04 +0200 paulson Konrad Slind's TFL
Fri, 18 Oct 1996 11:43:14 +0200 paulson New version of Yahalom, as recommended on p 259 of BAN paper
Fri, 18 Oct 1996 11:42:41 +0200 paulson Addition of Reveal message
Fri, 18 Oct 1996 11:42:17 +0200 paulson Deleted obsolete rewrites (they are now in HOL/simpdata)
Fri, 18 Oct 1996 11:41:41 +0200 paulson Reveal -> Revl
Fri, 18 Oct 1996 11:41:04 +0200 paulson The new proof of the lemma for new_nonces_not_seen is faster
Fri, 18 Oct 1996 11:39:55 +0200 paulson Generaly tidying up
Fri, 18 Oct 1996 11:39:10 +0200 paulson Important correction to comment
Fri, 18 Oct 1996 11:38:17 +0200 paulson Replaced excluded_middle_tac by case_tac; tidied proofs
Fri, 18 Oct 1996 11:37:19 +0200 paulson Tidied up the proof of A_trust_NS4
Fri, 18 Oct 1996 11:33:02 +0200 paulson Replaced excluded_middle_tac by case_tac
Fri, 18 Oct 1996 11:32:38 +0200 paulson Moving the CPUtimer declaration into cond_timeit should
Fri, 18 Oct 1996 11:31:33 +0200 paulson Now checks that $LISTEN is set
Wed, 16 Oct 1996 10:37:17 +0200 nipkow Defined pred using nat_case rather than nat_rec.
Tue, 15 Oct 1996 16:40:04 +0200 oheimb corrected `correction` of o_assoc (of version 1.14),
Tue, 15 Oct 1996 16:32:59 +0200 oheimb bound o_apply theorem to thy
Tue, 15 Oct 1996 10:58:59 +0200 paulson Removed extraneous spaces from all Makefiles
Tue, 15 Oct 1996 10:55:57 +0200 paulson changed prettyprinting of ==>
Tue, 15 Oct 1996 10:46:42 +0200 paulson Removed extraneous spaces from all Makefiles
Mon, 14 Oct 1996 11:08:54 +0200 paulson Removed call to obsolete totalCPUTimer function
Fri, 11 Oct 1996 10:55:03 +0200 paulson Addition of Sequents; removal of Modal and LK
Fri, 11 Oct 1996 10:52:54 +0200 paulson Addition of OtwayRees_AN
Thu, 10 Oct 1996 18:40:34 +0200 paulson Abadi and Needham's variant of Otway-Rees
Thu, 10 Oct 1996 12:00:23 +0200 paulson Deleted obsolete clasets
Thu, 10 Oct 1996 11:59:01 +0200 paulson Added comments describing better proofs
Thu, 10 Oct 1996 11:58:40 +0200 paulson Simpset removes the de Morgan laws
Thu, 10 Oct 1996 11:13:48 +0200 paulson Removed Modal since Sequents contains everything in it
Thu, 10 Oct 1996 11:09:03 +0200 paulson Removed LK since Sequents contains everything in it
Thu, 10 Oct 1996 10:57:33 +0200 paulson New root file with more description, and merging LK and Modal to Sequents
Thu, 10 Oct 1996 10:47:26 +0200 paulson Tidied some proofs: changed needed for de Morgan laws
Thu, 10 Oct 1996 10:46:14 +0200 paulson Addition of de Morgan laws
Thu, 10 Oct 1996 10:45:20 +0200 paulson Removed Fast_tac made redundant by addition of de Morgan laws
Wed, 09 Oct 1996 13:50:28 +0200 paulson Fuller description of examples
Wed, 09 Oct 1996 13:47:38 +0200 paulson Plain text README files now redundant due to HTML versions
Wed, 09 Oct 1996 13:43:51 +0200 paulson New version of axiom sees1_Says:
Wed, 09 Oct 1996 13:39:25 +0200 paulson Plain text README files now redundant due to HTML versions
Wed, 09 Oct 1996 13:38:11 +0200 paulson cond_timeit now catches exception Time, which sml/nj
Wed, 09 Oct 1996 13:37:00 +0200 paulson Updated references
(0) -1000 -300 -100 -60 +60 +100 +300 +1000 +3000 +10000 +30000 tip