* ZF: new-style theory commands '(co)inductive', '(co)datatype',
authorwenzelm
Thu Nov 15 18:34:58 2001 +0100 (2001-11-15)
changeset 122102f510d8d8291
parent 12209 09bc6f8456b9
child 12211 510c3eee55de
* 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');
NEWS
     1.1 --- a/NEWS	Thu Nov 15 18:21:38 2001 +0100
     1.2 +++ b/NEWS	Thu Nov 15 18:34:58 2001 +0100
     1.3 @@ -80,7 +80,7 @@
     1.4  multi-step methods like 'auto', 'simp_all', 'blast+' etc.;
     1.5  
     1.6  * Pure: proper integration with ``locales''; unlike the original
     1.7 -version by Florian Kammueller, Isar locales package high-level proof
     1.8 +version by Florian Kammüller, Isar locales package high-level proof
     1.9  contexts rather than raw logical ones (e.g. we admit to include
    1.10  attributes everywhere);
    1.11  
    1.12 @@ -191,7 +191,7 @@
    1.13  expressions;
    1.14  
    1.15  * HOL/GroupTheory: group theory examples including Sylow's theorem, by
    1.16 -Florian Kammüller;
    1.17 +Florian Kammüller;
    1.18  
    1.19  * HOL: got rid of some global declarations (potential INCOMPATIBILITY
    1.20  for ML tools): const "()" renamed "Product_Type.Unity", type "unit"
    1.21 @@ -209,8 +209,9 @@
    1.22  
    1.23  *** ZF ***
    1.24  
    1.25 -* ZF: new-style theory commands 'inductive', 'inductive_cases', and
    1.26 -methods 'ind_cases', 'induct_tac', 'case_tac';
    1.27 +* ZF: new-style theory commands '(co)inductive', '(co)datatype',
    1.28 +'rep_datatype', 'inductive_cases'; also methods 'ind_cases',
    1.29 +'induct_tac', 'case_tac', and 'typecheck' (with attribute 'TC');
    1.30  
    1.31  * ZF: the integer library now covers quotients and remainders, with
    1.32  many laws relating division to addition, multiplication, etc.;