# HG changeset patch
# User wenzelm
# Date 1005845698 -3600
# Node ID 2f510d8d8291a07c7cb19f2169ae5c1d9027c9f9
# Parent  09bc6f8456b99c63ed2d4f9f1043891e2dd16b9a
* 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');

diff -r 09bc6f8456b9 -r 2f510d8d8291 NEWS
--- a/NEWS	Thu Nov 15 18:21:38 2001 +0100
+++ b/NEWS	Thu Nov 15 18:34:58 2001 +0100
@@ -80,7 +80,7 @@
 multi-step methods like 'auto', 'simp_all', 'blast+' etc.;
 
 * Pure: proper integration with ``locales''; unlike the original
-version by Florian Kammueller, Isar locales package high-level proof
+version by Florian Kammüller, Isar locales package high-level proof
 contexts rather than raw logical ones (e.g. we admit to include
 attributes everywhere);
 
@@ -191,7 +191,7 @@
 expressions;
 
 * HOL/GroupTheory: group theory examples including Sylow's theorem, by
-Florian Kammüller;
+Florian Kammüller;
 
 * HOL: got rid of some global declarations (potential INCOMPATIBILITY
 for ML tools): const "()" renamed "Product_Type.Unity", type "unit"
@@ -209,8 +209,9 @@
 
 *** ZF ***
 
-* ZF: new-style theory commands 'inductive', 'inductive_cases', and
-methods 'ind_cases', 'induct_tac', 'case_tac';
+* 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');
 
 * ZF: the integer library now covers quotients and remainders, with
 many laws relating division to addition, multiplication, etc.;