NEWS

   - replace "#nnn" by "nnn", and "#-nnn" by "-nnn";
 
   - remove all special provisions on numerals in proofs;
 
 * HOL/record:
+  - removed old "make" and "make_scheme" operations -- INCOMPATIBILITY;
+  - removed "more" class (simply use "term") -- INCOMPATIBILITY;
   - provides cases/induct rules for use with corresponding Isar methods;
-  - old "make" and "make_scheme" operation removed -- INCOMPATIBILITY;
   - new derived operations "make" (for adding fields of current
     record), "extend" to promote fixed record to record scheme, and
     "truncate" for the reverse; cf. theorems "derived_defs", which are
     *not* declared as simp by default;
   - internal definitions directly based on a light-weight abstract

 
 * 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";