Thu, 15 Nov 2001 18:37:34 +0100 depends on Epsilon!
wenzelm [Thu, 15 Nov 2001 18:37:34 +0100] rev 12214
depends on Epsilon!
Thu, 15 Nov 2001 18:36:24 +0100 fix_frees: rev;
wenzelm [Thu, 15 Nov 2001 18:36:24 +0100] rev 12213
fix_frees: rev;
Thu, 15 Nov 2001 18:36:07 +0100 prove: raise ERROR_MESSAGE;
wenzelm [Thu, 15 Nov 2001 18:36:07 +0100] rev 12212
prove: raise ERROR_MESSAGE;
Thu, 15 Nov 2001 18:35:15 +0100 updated;
wenzelm [Thu, 15 Nov 2001 18:35:15 +0100] rev 12211
updated;
Thu, 15 Nov 2001 18:34:58 +0100 * ZF: new-style theory commands '(co)inductive', '(co)datatype',
wenzelm [Thu, 15 Nov 2001 18:34:58 +0100] rev 12210
* ZF: new-style theory commands '(co)inductive', '(co)datatype', 'rep_datatype', 'inductive_cases'; also methods 'ind_cases', 'induct_tac', 'case_tac', and 'typecheck' (with attribute 'TC');
Thu, 15 Nov 2001 18:21:38 +0100 type_solver_tac: use TCSET' to refer to context of goal state (does
wenzelm [Thu, 15 Nov 2001 18:21:38 +0100] rev 12209
type_solver_tac: use TCSET' to refer to context of goal state (does *not* work with local proof contexts of Isar / new-style locales);
Thu, 15 Nov 2001 18:20:48 +0100 setup DatatypeTactics.setup;
wenzelm [Thu, 15 Nov 2001 18:20:48 +0100] rev 12208
setup DatatypeTactics.setup;
Thu, 15 Nov 2001 18:20:13 +0100 added Induct/Binary_Trees.thy, Induct/Tree_Forest (converted from
wenzelm [Thu, 15 Nov 2001 18:20:13 +0100] rev 12207
added Induct/Binary_Trees.thy, Induct/Tree_Forest (converted from former ex/TF.ML ex/TF.thy ex/Term.ML ex/Term.thy);
Thu, 15 Nov 2001 18:18:17 +0100 no handle ERROR;
wenzelm [Thu, 15 Nov 2001 18:18:17 +0100] rev 12206
no handle ERROR;
Thu, 15 Nov 2001 18:16:17 +0100 fixed;
wenzelm [Thu, 15 Nov 2001 18:16:17 +0100] rev 12205
fixed;
(0) -10000 -3000 -1000 -300 -100 -10 +10 +100 +300 +1000 +3000 +10000 +30000 tip