NEWS
changeset 12622 7592926925d4
parent 12608 2df381faa787
child 12690 ac3fa7c05e5a
     1.1 --- a/NEWS	Thu Jan 03 17:48:02 2002 +0100
     1.2 +++ b/NEWS	Thu Jan 03 17:50:53 2002 +0100
     1.3 @@ -143,14 +143,6 @@
     1.4  * HOL: properly declared induction rules less_induct and
     1.5  wf_induct_rule;
     1.6  
     1.7 -* HOLCF: domain package adapted to new-style theory format, e.g. see
     1.8 -HOLCF/ex/Dnat.thy;
     1.9 -
    1.10 -* ZF: proper integration of logic-specific tools and packages,
    1.11 -including theory commands '(co)inductive', '(co)datatype',
    1.12 -'rep_datatype', 'inductive_cases', as well as methods 'ind_cases',
    1.13 -'induct_tac', 'case_tac', and 'typecheck' (with attribute 'TC');
    1.14 -
    1.15  
    1.16  *** HOL ***
    1.17  
    1.18 @@ -252,7 +244,13 @@
    1.19  
    1.20  *** HOLCF ***
    1.21  
    1.22 -* proper rep_datatype lift (see theory Lift) instead of ML hacks --
    1.23 +* Isar: consts/constdefs supports mixfix syntax for continuous
    1.24 +operations;
    1.25 +
    1.26 +* Isar: domain package adapted to new-style theory format, e.g. see
    1.27 +HOLCF/ex/Dnat.thy;
    1.28 +
    1.29 +* theory Lift: proper use of rep_datatype lift instead of ML hacks --
    1.30  potential INCOMPATIBILITY; now use plain induct_tac instead of former
    1.31  lift.induct_tac, always use UU instead of Undef;
    1.32  
    1.33 @@ -261,8 +259,16 @@
    1.34  
    1.35  *** ZF ***
    1.36  
    1.37 -* Theory Main no longer includes AC; for the Axiom of Choice, base your 
    1.38 -theory on Main_ZFC;
    1.39 +* Isar: proper integration of logic-specific tools and packages,
    1.40 +including theory commands '(co)inductive', '(co)datatype',
    1.41 +'rep_datatype', 'inductive_cases', as well as methods 'ind_cases',
    1.42 +'induct_tac', 'case_tac', and 'typecheck' (with attribute 'TC');
    1.43 +
    1.44 +* theory Main no longer includes AC; for the Axiom of Choice, base
    1.45 +your theory on Main_ZFC;
    1.46 +
    1.47 +* the integer library now covers quotients and remainders, with many
    1.48 +laws relating division to addition, multiplication, etc.;
    1.49  
    1.50  * ZF/UNITY: Chandy and Misra's UNITY is now available in ZF, giving a
    1.51  typeless version of the formalism;
    1.52 @@ -273,9 +279,6 @@
    1.53  including theory Multiset for multiset orderings; converted to
    1.54  new-style theory format;
    1.55  
    1.56 -* ZF: the integer library now covers quotients and remainders, with
    1.57 -many laws relating division to addition, multiplication, etc.;
    1.58 -
    1.59  
    1.60  *** General ***
    1.61  
    1.62 @@ -356,7 +359,7 @@
    1.63  
    1.64  * HOL: please note that theories in the Library and elsewhere often use the
    1.65  new-style (Isar) format; to refer to their theorems in an ML script you must
    1.66 -bind them to ML identifers by e.g.	val thm_name = thm "thm_name";
    1.67 +bind them to ML identifers by e.g.      val thm_name = thm "thm_name";
    1.68  
    1.69  * HOL: inductive package no longer splits induction rule aggressively,
    1.70  but only as far as specified by the introductions given; the old