| 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 |
| Wed, 14 Nov 2001 18:45:38 +0100 | wenzelm | store original simps for codegen; | changeset | files |
| Wed, 14 Nov 2001 18:44:27 +0100 | wenzelm | inductive: removed con_defs; | changeset | files |
| Wed, 14 Nov 2001 18:42:34 +0100 | wenzelm | updated; | changeset | files |
| Tue, 13 Nov 2001 22:36:38 +0100 | wenzelm | updated; | changeset | files |
| Tue, 13 Nov 2001 22:25:59 +0100 | wenzelm | * ZF: new-style theory commands 'inductive', 'inductive_cases', and | changeset | files |
| Tue, 13 Nov 2001 22:24:28 +0100 | wenzelm | ZF specific keywords; | changeset | files |