| Mon, 21 Sep 1998 23:25:27 +0200 | oheimb | *** empty log message *** | changeset | files |
| Mon, 21 Sep 1998 23:17:28 +0200 | oheimb | improved addbefore and addSbefore | changeset | files |
| Mon, 21 Sep 1998 23:16:25 +0200 | oheimb | *** empty log message *** | changeset | files |
| Mon, 21 Sep 1998 23:14:33 +0200 | oheimb | added addD2, addE2, addSD2, and addSE2 | changeset | files |
| Mon, 21 Sep 1998 23:13:28 +0200 | oheimb | improved indentation | changeset | files |
| Mon, 21 Sep 1998 23:12:31 +0200 | oheimb | added wrapper for bspec | changeset | files |
| Mon, 21 Sep 1998 23:06:37 +0200 | oheimb | added addD2, addE2, addSD2, and addSE2 | changeset | files |
| Mon, 21 Sep 1998 23:04:51 +0200 | oheimb | re-added mem and list_all | changeset | files |
| Mon, 21 Sep 1998 23:03:11 +0200 | oheimb | re-added mem and list_all | changeset | files |
| Mon, 21 Sep 1998 22:58:43 +0200 | oheimb | added dependance on HOL | changeset | files |
| Mon, 21 Sep 1998 15:58:27 +0200 | oheimb | added indentation | changeset | files |
| Mon, 21 Sep 1998 12:01:14 +0200 | oheimb | simplified proof | changeset | files |
| Mon, 21 Sep 1998 10:46:58 +0200 | paulson | inserted space in #-1 to prevent confusion with an integer constant | changeset | files |
| Mon, 21 Sep 1998 10:43:54 +0200 | paulson | Unary minus is now #- and not #~ | changeset | files |
| Mon, 21 Sep 1998 10:43:09 +0200 | paulson | much renaming and tidying | changeset | files |
| Fri, 18 Sep 1998 16:07:55 +0200 | paulson | leaves subgoal package empty | changeset | files |
| Fri, 18 Sep 1998 16:05:08 +0200 | paulson | improved (but still flawed) treatment of binary arithmetic | changeset | files |
| Fri, 18 Sep 1998 16:04:44 +0200 | paulson | Now defines "int" as a linear order; basic derivations moved to IntDef | changeset | files |
| 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 |