Tue, 12 Nov 1996 11:36:44 +0100 paulson Removed a call to polymorphic mem
Tue, 12 Nov 1996 11:36:18 +0100 paulson Added a comment
Mon, 11 Nov 1996 10:55:44 +0100 paulson Should never have been added in the first place
Fri, 08 Nov 1996 16:32:57 +0100 paulson A bit of tidying up
Fri, 08 Nov 1996 14:13:56 +0100 paulson Ran expandshort
Fri, 08 Nov 1996 14:07:56 +0100 paulson Removed "standard" call from uresult, to allow specialist applications
Fri, 08 Nov 1996 14:04:38 +0100 paulson Deleted a redundant pattern
Fri, 08 Nov 1996 14:02:51 +0100 paulson Adjusting to new version of uresult
Thu, 07 Nov 1996 10:19:15 +0100 paulson Tidying up: removing redundant assumptions, etc.
Thu, 07 Nov 1996 10:15:57 +0100 paulson Deleted bogus comment
Thu, 07 Nov 1996 10:11:06 +0100 paulson Adding lessI to default claset
Wed, 06 Nov 1996 12:49:31 +0100 wenzelm tuned fix_shyps a little bit more;
Tue, 05 Nov 1996 18:35:40 +0100 nipkow New version of paper.
Tue, 05 Nov 1996 11:48:09 +0100 paulson Replaced the very slow "find" command by "rm" with wildcards
Tue, 05 Nov 1996 11:20:52 +0100 paulson Simplified new_keys_not_seen, etc.: replaced the
Mon, 04 Nov 1996 17:23:37 +0100 nipkow Used nat_trans_tac. New Eta. various smaller changes.
Mon, 04 Nov 1996 10:56:15 +0100 paulson Renamed SELECT_GOAL's new parameter from x to selct to avoid clashes
Mon, 04 Nov 1996 10:54:26 +0100 paulson Removal of now unused sum, max, min. Use foldl op+, Int.max, Int.min
Fri, 01 Nov 1996 18:34:34 +0100 paulson Minor changes to comments
Fri, 01 Nov 1996 18:28:19 +0100 paulson New version with simpler disambiguation in YM3,
Fri, 01 Nov 1996 18:27:38 +0100 paulson New, purely illustrative result Crypt_synth_analz
Fri, 01 Nov 1996 15:46:56 +0100 paulson Proof of antisym_less_lift now simpler and more robust
Fri, 01 Nov 1996 15:45:50 +0100 paulson Now uses Int.max instead of max
Fri, 01 Nov 1996 15:42:40 +0100 paulson Changes tabs found in .thy files to spaces
Fri, 01 Nov 1996 15:41:09 +0100 paulson Replaced "sum" (only usage?) by foldl op+
Fri, 01 Nov 1996 15:39:37 +0100 paulson Now uses Int.max instead of max
Fri, 01 Nov 1996 15:37:30 +0100 paulson maxidx_of_typs replaces max o map maxidx_of_typ
Fri, 01 Nov 1996 15:35:28 +0100 paulson Now uses Int.max instead of max
Fri, 01 Nov 1996 15:32:03 +0100 paulson maxidx_of_typs replaces max o map maxidx_of_typ
Fri, 01 Nov 1996 15:30:49 +0100 paulson asm_rewrite_goal_tac now calls SELECT_GOAL.
Fri, 01 Nov 1996 15:25:21 +0100 paulson Replaced foldl nodup_TVars by nodup_TVars_list -- for a big speedup on Poly/ML
Fri, 01 Nov 1996 15:15:39 +0100 paulson Replaced min by Int.min
Fri, 01 Nov 1996 15:14:25 +0100 paulson Deleted Olist constructor. Replaced minidx by "above" function
Fri, 01 Nov 1996 15:12:21 +0100 paulson Now defines structure Int
Wed, 30 Oct 1996 11:21:24 +0100 paulson Changed some mem calls to mem_int for greater efficiency (not that it could matter)
Wed, 30 Oct 1996 11:20:27 +0100 paulson Only calls nodup_Vars if really necessary. We get a speedup of nearly 6%
Wed, 30 Oct 1996 11:19:09 +0100 paulson Changed some mem calls to mem_string for greater efficiency (not that it could matter)
Wed, 30 Oct 1996 11:17:54 +0100 paulson Minor updates
Wed, 30 Oct 1996 11:15:09 +0100 paulson Updated references
Mon, 28 Oct 1996 15:59:39 +0100 paulson Minor corrections
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)
(0) -1000 -300 -100 -60 +60 +100 +300 +1000 +3000 +10000 +30000 tip