NEWS

 
 better use "obtain" in situations as above; alternative refer to
 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);
 
 * Pure: theory goals now support ad-hoc contexts, which are discharged
 in the result, as in ``lemma (assumes A and B) K: A .''; syntax

 
 * HOL: syntax translations now work properly with numerals and records
 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"
 renamed "Product_Type.unit";
 

 HOLCF/ex/Dnat.thy;
 
 
 *** 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.;
 
 * ZF/Induct: new directory for examples of inductive definitions,