Thu, 10 Sep 1998 17:42:44 +0200 paulson eliminated equals0E
Thu, 10 Sep 1998 17:42:02 +0200 paulson fixed PROOF FAILED
Thu, 10 Sep 1998 17:40:03 +0200 paulson tidied
Thu, 10 Sep 1998 17:38:36 +0200 paulson deleted the bogus equals0E, fixed equals0D
Thu, 10 Sep 1998 17:36:42 +0200 paulson eliminated equals0E
Thu, 10 Sep 1998 17:34:43 +0200 paulson well-formed asym rules
Thu, 10 Sep 1998 17:34:01 +0200 paulson new file AC/WO1_WO7.thy
Thu, 10 Sep 1998 17:33:09 +0200 paulson Allows more backtracking in proof reconstruction, making it slower but more
Thu, 10 Sep 1998 17:32:07 +0200 paulson a step to help a proof
Thu, 10 Sep 1998 17:30:50 +0200 paulson new entries
Thu, 10 Sep 1998 17:30:24 +0200 paulson deleted not_Says_to_self
Thu, 10 Sep 1998 17:29:56 +0200 paulson well-formed asym rules; misc. tidying
Thu, 10 Sep 1998 17:28:36 +0200 paulson in_set_butlast_appendI supersedes in_set_butlast_appendI1,2
Thu, 10 Sep 1998 17:27:50 +0200 paulson tidied, fixing PROOF FAILED
Thu, 10 Sep 1998 17:27:15 +0200 paulson tidied
Thu, 10 Sep 1998 17:26:53 +0200 paulson tidied, eliminating hard proof
Thu, 10 Sep 1998 17:26:16 +0200 paulson well-formed zless_asym; tidied
Thu, 10 Sep 1998 17:25:13 +0200 paulson patch to stop failing proof
Thu, 10 Sep 1998 17:23:51 +0200 paulson New theorem wf_not_sym and well-formed wf_asym
Thu, 10 Sep 1998 17:23:16 +0200 paulson tided the unused rule irrefl_tranclI
Thu, 10 Sep 1998 17:20:49 +0200 paulson Changed equals0E back to equals0D and gave it the correct destruct form
Thu, 10 Sep 1998 17:17:22 +0200 paulson Adds order_refl, order_less_irrefl as simps, not as Iffs, to avoid PROOF FAILED
Thu, 10 Sep 1998 17:15:48 +0200 paulson in_set_butlast_appendI supersedes in_set_butlast_appendI1,2
Wed, 09 Sep 1998 17:34:58 +0200 nipkow Proved and added rewrite rule (@x. x=y) = y to simpset.
Wed, 09 Sep 1998 17:25:49 +0200 oheimb reflecting changes to Option.ML, List.{thy|ML}, mainly list_all
Wed, 09 Sep 1998 17:23:42 +0200 oheimb AddIffs[not_None_eq];
Wed, 09 Sep 1998 17:21:33 +0200 oheimb AddSDs[override_SomeD];
Wed, 09 Sep 1998 17:19:26 +0200 oheimb changed constants mem and list_all to mere translations
Wed, 09 Sep 1998 17:14:19 +0200 oheimb changed order of included theories
Wed, 09 Sep 1998 16:43:14 +0200 oheimb added Id_apply
Wed, 09 Sep 1998 16:42:45 +0200 oheimb removed superfluous AddIs thms (were already in)
Wed, 09 Sep 1998 16:21:08 +0200 oheimb renamed sswhen to sscase
Wed, 09 Sep 1998 16:13:35 +0200 oheimb simplified definition of axclass cpo
Tue, 08 Sep 1998 17:07:39 +0200 oheimb added caveat; a real solution would be difficult
Tue, 08 Sep 1998 17:03:21 +0200 oheimb improved spacing
Tue, 08 Sep 1998 16:06:04 +0200 oheimb adapted modifiers: Mod1 -> Mod2, Mod5 -> Mod4
Tue, 08 Sep 1998 15:17:11 +0200 paulson Got rid of not_Says_to_self and most uses of ~= in definitions and theorems
Tue, 08 Sep 1998 14:54:21 +0200 paulson Got rid of not_Says_to_self; re-organized proofs
Mon, 07 Sep 1998 10:46:48 +0200 paulson new example; tidying
Mon, 07 Sep 1998 10:45:45 +0200 paulson new example
Mon, 07 Sep 1998 10:43:31 +0200 paulson New UNITY theory, the N-S protocol
Mon, 07 Sep 1998 10:40:17 +0200 paulson tidying
Fri, 04 Sep 1998 13:24:10 +0200 nipkow Function 'upt'
Fri, 04 Sep 1998 11:01:59 +0200 nipkow Arith: less_diff_conv
Thu, 03 Sep 1998 16:40:02 +0200 paulson A new approach, using simp_of_act and simp_of_set to activate definitions when
Wed, 02 Sep 1998 16:52:06 +0200 nipkow Added function upto to List.
Wed, 02 Sep 1998 10:37:13 +0200 paulson modified proofs for new constrains_tac and ensures_tac
Wed, 02 Sep 1998 10:36:49 +0200 paulson two new thms
Wed, 02 Sep 1998 10:36:22 +0200 paulson Moved constrains_tac from SubstAx to Constrains.
Wed, 02 Sep 1998 10:35:11 +0200 paulson small simplification to not_Says_to_self
Tue, 01 Sep 1998 15:07:11 +0200 paulson New approach, using a locale
Tue, 01 Sep 1998 15:05:59 +0200 paulson tidied
Tue, 01 Sep 1998 15:05:36 +0200 paulson Replaced Suc_diff_n by Suc_diff_le
Tue, 01 Sep 1998 15:04:59 +0200 paulson new theory Induct/FoldSet
Tue, 01 Sep 1998 15:04:28 +0200 paulson New law card_Un_Int. Removed card_insert from simpset
Tue, 01 Sep 1998 15:03:43 +0200 paulson tidying; moved diff_less to Arith.ML
Tue, 01 Sep 1998 15:03:10 +0200 paulson changed Suc_diff_n to Suc_diff_le, with premise n <= m instead of n < Suc(m)
Tue, 01 Sep 1998 10:25:05 +0200 paulson New lemmas involving Int
Tue, 01 Sep 1998 10:11:06 +0200 paulson New lemmas involving Int
Tue, 01 Sep 1998 10:10:27 +0200 paulson fixed error msg
(0) -3000 -1000 -300 -100 -60 +60 +100 +300 +1000 +3000 +10000 +30000 tip