* Provers: 'simplified' attribute may refer to explicit rules instead
of full simplifier context; 'iff' attribute handles conditional rules;
* HOL/record:
- 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
theory of product types over typedef rather than datatype;

--- a/NEWS	Thu Oct 25 20:04:43 2001 +0200
+++ b/NEWS	Thu Oct 25 22:41:07 2001 +0200
@@ -58,6 +58,9 @@
 bound variables: "ALL x. P x --> Q x" (is "ALL x. _ --> ?C x")
 supersedes more cumbersome ... (is "ALL x. _ x --> ?C x");
 
+* Provers: 'simplified' attribute may refer to explicit rules instead
+of full simplifier context; 'iff' attribute handles conditional rules;
+
 * HOL: 'typedef' now allows alternative names for Rep/Abs morphisms;
 
 * HOL: 'recdef' now fails on unfinished automated proofs, use
@@ -98,8 +101,11 @@
 
 * HOL/record:
   - provides cases/induct rules for use with corresponding Isar methods;
-  - "record" operation truncates to particular fixed record (type cast);
-  - make_defs no longer part of default simps (INCOMPATIBILITY);
+  - 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
     theory of product types over typedef rather than datatype;