| Fri, 18 Sep 1998 16:04:00 +0200 | paulson | new files in Integ | changeset | files |
| Fri, 18 Sep 1998 15:15:40 +0200 | paulson | simpler definition of zmagnitude, and new thms for it | changeset | files |
| Fri, 18 Sep 1998 15:11:05 +0200 | paulson | stronger version of theI2 | changeset | files |
| Fri, 18 Sep 1998 15:09:46 +0200 | paulson | tidied | changeset | files |
| Fri, 18 Sep 1998 15:09:26 +0200 | paulson | new theorem less_imp_Suc_add | changeset | files |
| Fri, 18 Sep 1998 15:08:46 +0200 | paulson | new files in Integ | changeset | files |
| Fri, 18 Sep 1998 14:40:11 +0200 | paulson | new theorem less_Suc_eq_le | changeset | files |
| Fri, 18 Sep 1998 14:39:51 +0200 | paulson | new files in Integ | changeset | files |
| Fri, 18 Sep 1998 14:39:08 +0200 | paulson | new theorem less_Suc_eq_le and le_simps | changeset | files |
| Fri, 18 Sep 1998 14:36:54 +0200 | paulson | updated comments | changeset | files |
| Fri, 18 Sep 1998 14:36:36 +0200 | paulson | tidying | changeset | files |
| Fri, 18 Sep 1998 14:36:03 +0200 | paulson | theorem le_diff_conv2; tidying and expandshort | changeset | files |
| Fri, 18 Sep 1998 14:34:06 +0200 | paulson | Pruning of parameters and True assumptions | changeset | files |
| Fri, 18 Sep 1998 14:33:20 +0200 | paulson | Suppress timing messages for theorems proved in theory sections | changeset | files |
| Fri, 18 Sep 1998 14:32:49 +0200 | paulson | improved error messages | changeset | files |
| Wed, 16 Sep 1998 10:28:54 +0200 | paulson | deleted redundant quantifiers | changeset | files |
| Tue, 15 Sep 1998 15:10:38 +0200 | paulson | From Compl(A) to -A | changeset | files |
| Tue, 15 Sep 1998 15:06:29 +0200 | paulson | revised treatment of integers | changeset | files |
| Tue, 15 Sep 1998 15:04:07 +0200 | paulson | From Compl(A) to -A | changeset | files |
| Tue, 15 Sep 1998 13:09:23 +0200 | nipkow | Function 'step' is already defined in NA.thy. | changeset | files |
| Tue, 15 Sep 1998 10:40:40 +0200 | paulson | tidied | changeset | files |
| Mon, 14 Sep 1998 10:18:07 +0200 | paulson | commented out duplicate proof | changeset | files |
| Mon, 14 Sep 1998 10:17:44 +0200 | paulson | simpler proof | changeset | files |
| Mon, 14 Sep 1998 10:17:19 +0200 | paulson | new theorem le_diff_conv | changeset | files |
| Fri, 11 Sep 1998 18:09:54 +0200 | paulson | Extra steps at end to make it run faster | changeset | files |
| Fri, 11 Sep 1998 17:20:58 +0200 | oheimb | added clarsimp_tac and Clarsimp_tac | changeset | files |
| Fri, 11 Sep 1998 16:32:31 +0200 | paulson | tidied using locales | changeset | files |
| Fri, 11 Sep 1998 16:31:40 +0200 | paulson | Less deterministic reconstruction: now more robust but perhaps slower | changeset | files |
| Fri, 11 Sep 1998 16:26:22 +0200 | paulson | tidied | changeset | files |
| Fri, 11 Sep 1998 16:25:40 +0200 | paulson | fixed PROOF FAILED | changeset | files |
| Fri, 11 Sep 1998 16:25:24 +0200 | paulson | fixed comment | changeset | files |
| Fri, 11 Sep 1998 14:09:46 +0200 | oheimb | stabilized proof of card_mono | changeset | files |
| Fri, 11 Sep 1998 12:55:40 +0200 | oheimb | corrected indentation | changeset | files |
| Thu, 10 Sep 1998 18:07:06 +0200 | paulson | equals0D | changeset | files |
| Thu, 10 Sep 1998 18:06:39 +0200 | paulson | well-formed asym rules; also adds less_irrefl, le_refl since order_refl | changeset | files |
| Thu, 10 Sep 1998 17:50:06 +0200 | paulson | added proof of final result... | changeset | files |
| Thu, 10 Sep 1998 17:49:36 +0200 | paulson | tidied | changeset | files |
| Thu, 10 Sep 1998 17:49:14 +0200 | paulson | Now WO1_WO7 has a .thy file | changeset | files |
| Thu, 10 Sep 1998 17:42:44 +0200 | paulson | eliminated equals0E | changeset | files |
| Thu, 10 Sep 1998 17:42:02 +0200 | paulson | fixed PROOF FAILED | changeset | files |
| Thu, 10 Sep 1998 17:40:03 +0200 | paulson | tidied | changeset | files |
| Thu, 10 Sep 1998 17:38:36 +0200 | paulson | deleted the bogus equals0E, fixed equals0D | changeset | files |
| Thu, 10 Sep 1998 17:36:42 +0200 | paulson | eliminated equals0E | changeset | files |
| Thu, 10 Sep 1998 17:34:43 +0200 | paulson | well-formed asym rules | changeset | files |
| Thu, 10 Sep 1998 17:34:01 +0200 | paulson | new file AC/WO1_WO7.thy | changeset | files |
| Thu, 10 Sep 1998 17:33:09 +0200 | paulson | Allows more backtracking in proof reconstruction, making it slower but more | changeset | files |
| Thu, 10 Sep 1998 17:32:07 +0200 | paulson | a step to help a proof | changeset | files |
| Thu, 10 Sep 1998 17:30:50 +0200 | paulson | new entries | changeset | files |
| Thu, 10 Sep 1998 17:30:24 +0200 | paulson | deleted not_Says_to_self | changeset | files |
| Thu, 10 Sep 1998 17:29:56 +0200 | paulson | well-formed asym rules; misc. tidying | changeset | files |
| Thu, 10 Sep 1998 17:28:36 +0200 | paulson | in_set_butlast_appendI supersedes in_set_butlast_appendI1,2 | changeset | files |
| Thu, 10 Sep 1998 17:27:50 +0200 | paulson | tidied, fixing PROOF FAILED | changeset | files |
| Thu, 10 Sep 1998 17:27:15 +0200 | paulson | tidied | changeset | files |
| Thu, 10 Sep 1998 17:26:53 +0200 | paulson | tidied, eliminating hard proof | changeset | files |
| Thu, 10 Sep 1998 17:26:16 +0200 | paulson | well-formed zless_asym; tidied | changeset | files |
| Thu, 10 Sep 1998 17:25:13 +0200 | paulson | patch to stop failing proof | changeset | files |
| Thu, 10 Sep 1998 17:23:51 +0200 | paulson | New theorem wf_not_sym and well-formed wf_asym | changeset | files |
| Thu, 10 Sep 1998 17:23:16 +0200 | paulson | tided the unused rule irrefl_tranclI | changeset | files |
| Thu, 10 Sep 1998 17:20:49 +0200 | paulson | Changed equals0E back to equals0D and gave it the correct destruct form | changeset | files |
| Thu, 10 Sep 1998 17:17:22 +0200 | paulson | Adds order_refl, order_less_irrefl as simps, not as Iffs, to avoid PROOF FAILED | changeset | files |