| 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 |
| Fri, 16 Nov 2001 22:10:27 +0100 | wenzelm | converted; | changeset | files |
| Fri, 16 Nov 2001 22:09:44 +0100 | wenzelm | actually store "coinduct" rule; | changeset | files |
| Fri, 16 Nov 2001 22:08:55 +0100 | wenzelm | additional P.marg_comment; | changeset | files |
| Fri, 16 Nov 2001 22:08:28 +0100 | wenzelm | \usepackage[latin1]{inputenc}; | changeset | files |
| Fri, 16 Nov 2001 18:24:11 +0100 | paulson | even more theories from Jacques | changeset | files |
| Fri, 16 Nov 2001 15:25:17 +0100 | wenzelm | finish_global: Drule.strip_shyps_warning (just for warning); | changeset | files |
| Fri, 16 Nov 2001 15:24:39 +0100 | wenzelm | ext_tsig_classes: rebuild_tsig!!!!! | changeset | files |
| Fri, 16 Nov 2001 15:24:09 +0100 | wenzelm | local_standard: plain strip_shyps instead of strip_shyps_warning; | changeset | files |
| Fri, 16 Nov 2001 13:48:43 +0100 | paulson | last-minute tidying | changeset | files |
| Thu, 15 Nov 2001 23:26:58 +0100 | wenzelm | updated; | changeset | files |
| Thu, 15 Nov 2001 23:25:46 +0100 | wenzelm | GPLed; | changeset | files |
| Thu, 15 Nov 2001 23:25:01 +0100 | wenzelm | write_keywords: string argument (logic name); | changeset | files |
| Thu, 15 Nov 2001 23:21:57 +0100 | wenzelm | isatool unsymbolize; | changeset | files |
| Thu, 15 Nov 2001 20:01:19 +0100 | ehmety | Modified to make the files build with the new changes in ZF | changeset | files |
| Thu, 15 Nov 2001 18:37:34 +0100 | wenzelm | depends on Epsilon! | changeset | files |
| Thu, 15 Nov 2001 18:36:24 +0100 | wenzelm | fix_frees: rev; | changeset | files |
| Thu, 15 Nov 2001 18:36:07 +0100 | wenzelm | prove: raise ERROR_MESSAGE; | changeset | files |
| Thu, 15 Nov 2001 18:35:15 +0100 | wenzelm | updated; | changeset | files |
| Thu, 15 Nov 2001 18:34:58 +0100 | wenzelm | * ZF: new-style theory commands '(co)inductive', '(co)datatype', | changeset | files |
| Thu, 15 Nov 2001 18:21:38 +0100 | wenzelm | type_solver_tac: use TCSET' to refer to context of goal state (does | changeset | files |
| Thu, 15 Nov 2001 18:20:48 +0100 | wenzelm | setup DatatypeTactics.setup; | changeset | files |
| Thu, 15 Nov 2001 18:20:13 +0100 | wenzelm | added Induct/Binary_Trees.thy, Induct/Tree_Forest (converted from | changeset | files |
| Thu, 15 Nov 2001 18:18:17 +0100 | wenzelm | no handle ERROR; | changeset | files |
| Thu, 15 Nov 2001 18:16:17 +0100 | wenzelm | fixed; | changeset | files |
| Thu, 15 Nov 2001 18:15:58 +0100 | wenzelm | Isar version of 'rep_datatype'; | changeset | files |
| Thu, 15 Nov 2001 18:15:32 +0100 | wenzelm | avoid handle _; | changeset | files |
| Thu, 15 Nov 2001 18:15:13 +0100 | wenzelm | added TCSET(') tacticals; | changeset | files |
| Thu, 15 Nov 2001 18:09:40 +0100 | wenzelm | added Term and Tree_Forest (from converted ZF/ex); | changeset | files |
| Thu, 15 Nov 2001 18:08:19 +0100 | wenzelm | TF and Term moved to ZF/Induct; | changeset | files |
| Thu, 15 Nov 2001 17:59:56 +0100 | paulson | miniscoping of UN and INT | changeset | files |
| Thu, 15 Nov 2001 16:48:05 +0100 | ehmety | Added new entry | changeset | files |
| Thu, 15 Nov 2001 16:46:38 +0100 | ehmety | New files | changeset | files |
| Thu, 15 Nov 2001 16:12:49 +0100 | paulson | new theories from Jacques Fleuriot | changeset | files |
| Thu, 15 Nov 2001 15:07:16 +0100 | ehmety | *** empty log message *** | changeset | files |
| Wed, 14 Nov 2001 23:22:43 +0100 | wenzelm | converted datatype examples moved from ZF/ex to ZF/Induct; | changeset | files |
| Wed, 14 Nov 2001 23:22:15 +0100 | wenzelm | document setup; | changeset | files |
| Wed, 14 Nov 2001 23:21:05 +0100 | wenzelm | removed BT, Data, Enum (see ZF/Induct); | changeset | files |
| Wed, 14 Nov 2001 23:20:41 +0100 | wenzelm | case_names; | changeset | files |
| Wed, 14 Nov 2001 23:20:14 +0100 | wenzelm | added Datatypes, Binary_Trees (from ZF/ex); | changeset | files |
| Wed, 14 Nov 2001 23:19:09 +0100 | wenzelm | Isar attribute and method setup; | changeset | files |
| Wed, 14 Nov 2001 23:18:37 +0100 | wenzelm | fix path prefix; | changeset | files |
| Wed, 14 Nov 2001 23:18:13 +0100 | wenzelm | use proper intr_names (for required case_names); | changeset | files |
| Wed, 14 Nov 2001 23:16:05 +0100 | wenzelm | added Induct/Binary_Trees.thy, Induct/Datatypes.thy; | changeset | files |
| Wed, 14 Nov 2001 23:15:19 +0100 | wenzelm | tuned; | changeset | files |
| Wed, 14 Nov 2001 23:14:59 +0100 | wenzelm | updated; | changeset | files |
| Wed, 14 Nov 2001 18:46:30 +0100 | wenzelm | adapted primrec/datatype to Isar; | changeset | files |
| Wed, 14 Nov 2001 18:46:07 +0100 | wenzelm | tuned; | changeset | files |