| Sat, 26 Sep 1998 16:13:05 +0200 | berghofe | Package now chooses type variable names more carefully to | changeset | files |
| Fri, 25 Sep 1998 16:21:56 +0200 | oheimb | minor corrections | changeset | files |
| Fri, 25 Sep 1998 15:57:23 +0200 | oheimb | exchanged automatic-tactics and semi-automatic-tactics | changeset | files |
| Fri, 25 Sep 1998 15:54:29 +0200 | oheimb | improved indentation | changeset | files |
| Fri, 25 Sep 1998 15:21:07 +0200 | wenzelm | rearranged SIMPSET('); | changeset | files |
| Fri, 25 Sep 1998 14:54:49 +0200 | wenzelm | *** empty log message *** | changeset | files |
| Fri, 25 Sep 1998 14:49:12 +0200 | wenzelm | isatool logo; | changeset | files |
| Fri, 25 Sep 1998 14:47:39 +0200 | wenzelm | added isatool logo; | changeset | files |
| Fri, 25 Sep 1998 14:32:36 +0200 | wenzelm | improved; | changeset | files |
| Fri, 25 Sep 1998 14:06:56 +0200 | paulson | Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants | changeset | files |
| Fri, 25 Sep 1998 14:06:27 +0200 | paulson | added Int to BasisLibrary | changeset | files |
| Fri, 25 Sep 1998 14:06:00 +0200 | paulson | deleted illegal "op" | changeset | files |
| Fri, 25 Sep 1998 14:05:34 +0200 | paulson | uses BasisLibrary for Int.min | changeset | files |
| Fri, 25 Sep 1998 14:05:13 +0200 | paulson | patched obsolete code | changeset | files |
| Fri, 25 Sep 1998 14:04:22 +0200 | paulson | Renaming of Integ/Integ.* to Integ/Int.* | changeset | files |
| Fri, 25 Sep 1998 13:58:24 +0200 | paulson | Now uses integers instead of naturals | changeset | files |
| Fri, 25 Sep 1998 13:57:01 +0200 | paulson | Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants | changeset | files |
| Fri, 25 Sep 1998 13:18:07 +0200 | paulson | Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants | changeset | files |
| Fri, 25 Sep 1998 12:12:07 +0200 | wenzelm | tuned; | changeset | files |
| Fri, 25 Sep 1998 12:03:11 +0200 | wenzelm | tuned pretty_tag; | changeset | files |
| Fri, 25 Sep 1998 12:01:47 +0200 | wenzelm | added REPEAT1; | changeset | files |
| Thu, 24 Sep 1998 21:32:12 +0200 | wenzelm | create an instance of the Isabelle logo; | changeset | files |
| Thu, 24 Sep 1998 21:19:01 +0200 | wenzelm | generic eps version; | changeset | files |
| Thu, 24 Sep 1998 17:18:33 +0200 | oheimb | simplified CLASIMP_DATA | changeset | files |
| Thu, 24 Sep 1998 17:17:56 +0200 | oheimb | removed addcongs2 and delcongs2 | changeset | files |
| Thu, 24 Sep 1998 17:17:14 +0200 | oheimb | renamed mk_meta_eq to mk_eq | changeset | files |
| Thu, 24 Sep 1998 17:16:06 +0200 | oheimb | simplified CLASIMP_DATA | changeset | files |
| Thu, 24 Sep 1998 17:07:24 +0200 | paulson | renamed some axioms; some new theorems | changeset | files |
| Thu, 24 Sep 1998 16:53:14 +0200 | oheimb | introduced addSE2, addSD2, addE2, and addD2 | changeset | files |
| Thu, 24 Sep 1998 16:53:00 +0200 | oheimb | improved description of looper and splitter | changeset | files |
| Thu, 24 Sep 1998 15:36:16 +0200 | oheimb | workaround for litte bug in our ln command | changeset | files |
| Thu, 24 Sep 1998 15:23:47 +0200 | paulson | Function nat_of now maps negative integers to zero, not their absolute value | changeset | files |
| Thu, 24 Sep 1998 15:21:30 +0200 | paulson | renamed some axioms | changeset | files |
| Thu, 24 Sep 1998 15:20:29 +0200 | paulson | added correctness proofs for arithmetic | changeset | files |
| Thu, 24 Sep 1998 15:20:03 +0200 | paulson | new induction rule for integers | changeset | files |
| Thu, 24 Sep 1998 11:00:07 +0200 | oheimb | fixed calls of ln, rm | changeset | files |
| Wed, 23 Sep 1998 12:44:30 +0200 | wenzelm | changed xnum token syntax; | changeset | files |
| Wed, 23 Sep 1998 10:56:08 +0200 | paulson | unary minus | changeset | files |
| Wed, 23 Sep 1998 10:25:37 +0200 | paulson | much renaming and reorganization | changeset | files |
| Wed, 23 Sep 1998 10:17:11 +0200 | paulson | New directory Integ for the integers | changeset | files |
| Wed, 23 Sep 1998 10:15:09 +0200 | paulson | a few new theorems | changeset | files |
| Wed, 23 Sep 1998 10:12:01 +0200 | paulson | deleted needless parentheses | changeset | files |
| Wed, 23 Sep 1998 10:11:18 +0200 | paulson | tidying and deleting needless parentheses | changeset | files |
| Wed, 23 Sep 1998 10:03:32 +0200 | paulson | deleted needless parentheses | changeset | files |
| Tue, 22 Sep 1998 17:08:30 +0200 | wenzelm | tuned Isamode; | changeset | files |
| Tue, 22 Sep 1998 15:24:39 +0200 | paulson | re-organized for the new directory Integ | changeset | files |
| Tue, 22 Sep 1998 15:24:01 +0200 | paulson | new directory for Integers | changeset | files |
| Tue, 22 Sep 1998 15:23:39 +0200 | paulson | deleted erroneous semicolon | changeset | files |
| Tue, 22 Sep 1998 15:22:18 +0200 | paulson | tidying | changeset | files |
| Tue, 22 Sep 1998 13:50:57 +0200 | paulson | tidying | changeset | files |
| Tue, 22 Sep 1998 13:49:22 +0200 | paulson | new directory for Integers | changeset | files |
| Tue, 22 Sep 1998 13:48:32 +0200 | paulson | big tidying of simpsets, etc | changeset | files |
| 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 |
| 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 |