wenzelm [Thu, 15 Nov 2001 23:25:46 +0100] rev 12218
GPLed;
wenzelm [Thu, 15 Nov 2001 23:25:01 +0100] rev 12217
write_keywords: string argument (logic name);
wenzelm [Thu, 15 Nov 2001 23:21:57 +0100] rev 12216
isatool unsymbolize;
ehmety [Thu, 15 Nov 2001 20:01:19 +0100] rev 12215
Modified to make the files build with the new changes in ZF
wenzelm [Thu, 15 Nov 2001 18:37:34 +0100] rev 12214
depends on Epsilon!
wenzelm [Thu, 15 Nov 2001 18:36:24 +0100] rev 12213
fix_frees: rev;
wenzelm [Thu, 15 Nov 2001 18:36:07 +0100] rev 12212
prove: raise ERROR_MESSAGE;
wenzelm [Thu, 15 Nov 2001 18:35:15 +0100] rev 12211
updated;
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');
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);