| 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 |