# HG changeset patch
# User wenzelm
# Date 1004032740 -7200
# Node ID acfea249b03cad8f5762b64db97e229d95e5e159
# Parent  c1c4890a1ecbf62a2b39a072595c777fc525f350
tuned;

diff -r c1c4890a1ecb -r acfea249b03c NEWS
--- a/NEWS	Thu Oct 25 19:55:41 2001 +0200
+++ b/NEWS	Thu Oct 25 19:59:00 2001 +0200
@@ -54,8 +54,8 @@
 
 * Pure: removed obsolete 'exported' attribute;
 
-* Pure: dummy pattern "_" in is/let is now automatically ``lifted''
-over bound variables: "ALL x. P x --> Q x" (is "ALL x. _ --> ?C x")
+* Pure: dummy pattern "_" in is/let is now automatically lifted over
+bound variables: "ALL x. P x --> Q x" (is "ALL x. _ --> ?C x")
 supersedes more cumbersome ... (is "ALL x. _ x --> ?C x");
 
 * HOL: 'typedef' now allows alternative names for Rep/Abs morphisms;
@@ -63,10 +63,9 @@
 * HOL: 'recdef' now fails on unfinished automated proofs, use
 "(permissive)" option to recover old behavior;
 
-* HOL: 'inductive' now longer features separate (collective)
-attributes for 'intros';
-
-* HOL: canonical cases/induct rules for n-tuples (n = 3..7);
+* HOL: 'inductive' no longer features separate (collective) attributes
+for 'intros' (was found too confusing);
+
 
 
 *** HOL ***
@@ -99,12 +98,13 @@
 
 * HOL/record:
   - provides cases/induct rules for use with corresponding Isar methods;
-  - "record" operation truncates to particular fixed record (acts like
-    a type cast);
-  - make_defs no longer part of default simps;
+  - "record" operation truncates to particular fixed record (type cast);
+  - make_defs no longer part of default simps (INCOMPATIBILITY);
   - internal definitions directly based on a light-weight abstract
     theory of product types over typedef rather than datatype;
 
+* HOL: canonical cases/induct rules for n-tuples (n = 3..7);
+
 * HOL: concrete setsum syntax "\<Sum>i:A. b" == "setsum (%i. b) A"
 (beware of argument permutation!);
 
@@ -133,10 +133,9 @@
 * HOL/GroupTheory: group theory examples including Sylow's theorem, by
 Florian Kammüller;
 
-* HOL: eliminated global items
-
-  const "()" -> "Product_Type.Unity"
-  type "unit" -> "Product_Type.unit"
+* HOL: got rid of some global declarations (potential INCOMPATIBILITY
+for ML tools): const "()" renamed "Product_Type.Unity", type "unit"
+renamed "Product_Type.unit";
 
 
 *** ZF ***