| Tue, 20 Nov 2001 20:57:46 +0100 | wenzelm | prefer later trfuns; | changeset | files |
| Tue, 20 Nov 2001 20:57:07 +0100 | wenzelm | moved prefixes1, suffixes1 to library.ML; | changeset | files |
| Tue, 20 Nov 2001 20:56:42 +0100 | wenzelm | trfuns *after* binder syntax; | changeset | files |
| Tue, 20 Nov 2001 20:56:13 +0100 | wenzelm | added prefixes1, suffixes1; | changeset | files |
| Tue, 20 Nov 2001 20:55:50 +0100 | wenzelm | print_depth 10; | changeset | files |
| Tue, 20 Nov 2001 20:55:33 +0100 | wenzelm | derive cases/induct rules for ``more'' parts; | changeset | files |
| Tue, 20 Nov 2001 20:54:12 +0100 | wenzelm | tuned; | changeset | files |
| Tue, 20 Nov 2001 10:48:38 +0100 | paulson | Hyperreal | changeset | files |
| Mon, 19 Nov 2001 23:37:01 +0100 | wenzelm | improved treatment of common result name; | changeset | files |
| Mon, 19 Nov 2001 20:47:57 +0100 | wenzelm | tuned; | changeset | files |
| Mon, 19 Nov 2001 20:47:39 +0100 | wenzelm | multi_theorem: common statement header (covers *all* results); | changeset | files |
| Mon, 19 Nov 2001 20:46:38 +0100 | wenzelm | fixed comment; | changeset | files |
| Mon, 19 Nov 2001 20:46:05 +0100 | wenzelm | induct method: localize rews for rule; | changeset | files |
| Mon, 19 Nov 2001 17:42:00 +0100 | berghofe | Now handles different theorems with same name more gracefully. | changeset | files |
| Mon, 19 Nov 2001 17:40:45 +0100 | berghofe | Improved error message. | changeset | files |
| Mon, 19 Nov 2001 17:40:07 +0100 | berghofe | Added setup. | changeset | files |
| Mon, 19 Nov 2001 17:39:31 +0100 | berghofe | Moved fastype to Envir. | changeset | files |
| Mon, 19 Nov 2001 17:38:09 +0100 | berghofe | Further restructuring of theorem naming functions. | changeset | files |
| Mon, 19 Nov 2001 17:36:40 +0100 | berghofe | Added setup for proof rewrite rules. | changeset | files |
| Mon, 19 Nov 2001 17:36:05 +0100 | berghofe | - Fixed bug in shrink | changeset | files |
| Mon, 19 Nov 2001 17:34:02 +0100 | berghofe | Replaced devar by Envir.head_norm | changeset | files |
| Mon, 19 Nov 2001 17:32:49 +0100 | berghofe | Moved head_norm and fastype from unify.ML to envir.ML | changeset | files |
| Fri, 16 Nov 2001 23:02:58 +0100 | kleing | fixed maxs bug | changeset | files |
| Fri, 16 Nov 2001 22:11:19 +0100 | wenzelm | Ntree and Brouwer converted and moved to ZF/Induct; | changeset | files |