1.1 --- a/NEWS	Thu Oct 25 22:41:07 2001 +0200
     1.2 +++ b/NEWS	Thu Oct 25 22:42:12 2001 +0200
     1.3 @@ -100,8 +100,9 @@
     1.4    - remove all special provisions on numerals in proofs;
     1.5  
     1.6  * HOL/record:
     1.7 +  - removed old "make" and "make_scheme" operations -- INCOMPATIBILITY;
     1.8 +  - removed "more" class (simply use "term") -- INCOMPATIBILITY;
     1.9    - provides cases/induct rules for use with corresponding Isar methods;
    1.10 -  - old "make" and "make_scheme" operation removed -- INCOMPATIBILITY;
    1.11    - new derived operations "make" (for adding fields of current
    1.12      record), "extend" to promote fixed record to record scheme, and
    1.13      "truncate" for the reverse; cf. theorems "derived_defs", which are
    1.14 @@ -137,7 +138,7 @@
    1.15  expressions;
    1.16  
    1.17  * HOL/GroupTheory: group theory examples including Sylow's theorem, by
    1.18 -Florian Kammüller;
    1.19 +Florian Kammüller;
    1.20  
    1.21  * HOL: got rid of some global declarations (potential INCOMPATIBILITY
    1.22  for ML tools): const "()" renamed "Product_Type.Unity", type "unit"