Fri, 18 Sep 1998 14:40:11 +0200 paulson new theorem less_Suc_eq_le
Fri, 18 Sep 1998 14:39:51 +0200 paulson new files in Integ
Fri, 18 Sep 1998 14:39:08 +0200 paulson new theorem less_Suc_eq_le and le_simps
Fri, 18 Sep 1998 14:36:54 +0200 paulson updated comments
Fri, 18 Sep 1998 14:36:36 +0200 paulson tidying
Fri, 18 Sep 1998 14:36:03 +0200 paulson theorem le_diff_conv2; tidying and expandshort
Fri, 18 Sep 1998 14:34:06 +0200 paulson Pruning of parameters and True assumptions
Fri, 18 Sep 1998 14:33:20 +0200 paulson Suppress timing messages for theorems proved in theory sections
Fri, 18 Sep 1998 14:32:49 +0200 paulson improved error messages
Wed, 16 Sep 1998 10:28:54 +0200 paulson deleted redundant quantifiers
Tue, 15 Sep 1998 15:10:38 +0200 paulson From Compl(A) to -A
Tue, 15 Sep 1998 15:06:29 +0200 paulson revised treatment of integers
Tue, 15 Sep 1998 15:04:07 +0200 paulson From Compl(A) to -A
Tue, 15 Sep 1998 13:09:23 +0200 nipkow Function 'step' is already defined in NA.thy.
Tue, 15 Sep 1998 10:40:40 +0200 paulson tidied
Mon, 14 Sep 1998 10:18:07 +0200 paulson commented out duplicate proof
Mon, 14 Sep 1998 10:17:44 +0200 paulson simpler proof
Mon, 14 Sep 1998 10:17:19 +0200 paulson new theorem le_diff_conv
Fri, 11 Sep 1998 18:09:54 +0200 paulson Extra steps at end to make it run faster
Fri, 11 Sep 1998 17:20:58 +0200 oheimb added clarsimp_tac and Clarsimp_tac
Fri, 11 Sep 1998 16:32:31 +0200 paulson tidied using locales
Fri, 11 Sep 1998 16:31:40 +0200 paulson Less deterministic reconstruction: now more robust but perhaps slower
Fri, 11 Sep 1998 16:26:22 +0200 paulson tidied
Fri, 11 Sep 1998 16:25:40 +0200 paulson fixed PROOF FAILED
Fri, 11 Sep 1998 16:25:24 +0200 paulson fixed comment
Fri, 11 Sep 1998 14:09:46 +0200 oheimb stabilized proof of card_mono
Fri, 11 Sep 1998 12:55:40 +0200 oheimb corrected indentation
Thu, 10 Sep 1998 18:07:06 +0200 paulson equals0D
Thu, 10 Sep 1998 18:06:39 +0200 paulson well-formed asym rules; also adds less_irrefl, le_refl since order_refl
Thu, 10 Sep 1998 17:50:06 +0200 paulson added proof of final result...
Thu, 10 Sep 1998 17:49:36 +0200 paulson tidied
Thu, 10 Sep 1998 17:49:14 +0200 paulson Now WO1_WO7 has a .thy file
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
(0) -3000 -1000 -300 -100 -60 +60 +100 +300 +1000 +3000 +10000 +30000 tip