1.1 --- a/NEWS	Thu Oct 25 19:55:41 2001 +0200
     1.2 +++ b/NEWS	Thu Oct 25 19:59:00 2001 +0200
     1.3 @@ -54,8 +54,8 @@
     1.4  
     1.5  * Pure: removed obsolete 'exported' attribute;
     1.6  
     1.7 -* Pure: dummy pattern "_" in is/let is now automatically ``lifted''
     1.8 -over bound variables: "ALL x. P x --> Q x" (is "ALL x. _ --> ?C x")
     1.9 +* Pure: dummy pattern "_" in is/let is now automatically lifted over
    1.10 +bound variables: "ALL x. P x --> Q x" (is "ALL x. _ --> ?C x")
    1.11  supersedes more cumbersome ... (is "ALL x. _ x --> ?C x");
    1.12  
    1.13  * HOL: 'typedef' now allows alternative names for Rep/Abs morphisms;
    1.14 @@ -63,10 +63,9 @@
    1.15  * HOL: 'recdef' now fails on unfinished automated proofs, use
    1.16  "(permissive)" option to recover old behavior;
    1.17  
    1.18 -* HOL: 'inductive' now longer features separate (collective)
    1.19 -attributes for 'intros';
    1.20 -
    1.21 -* HOL: canonical cases/induct rules for n-tuples (n = 3..7);
    1.22 +* HOL: 'inductive' no longer features separate (collective) attributes
    1.23 +for 'intros' (was found too confusing);
    1.24 +
    1.25  
    1.26  
    1.27  *** HOL ***
    1.28 @@ -99,12 +98,13 @@
    1.29  
    1.30  * HOL/record:
    1.31    - provides cases/induct rules for use with corresponding Isar methods;
    1.32 -  - "record" operation truncates to particular fixed record (acts like
    1.33 -    a type cast);
    1.34 -  - make_defs no longer part of default simps;
    1.35 +  - "record" operation truncates to particular fixed record (type cast);
    1.36 +  - make_defs no longer part of default simps (INCOMPATIBILITY);
    1.37    - internal definitions directly based on a light-weight abstract
    1.38      theory of product types over typedef rather than datatype;
    1.39  
    1.40 +* HOL: canonical cases/induct rules for n-tuples (n = 3..7);
    1.41 +
    1.42  * HOL: concrete setsum syntax "\<Sum>i:A. b" == "setsum (%i. b) A"
    1.43  (beware of argument permutation!);
    1.44  
    1.45 @@ -133,10 +133,9 @@
    1.46  * HOL/GroupTheory: group theory examples including Sylow's theorem, by
    1.47  Florian Kammüller;
    1.48  
    1.49 -* HOL: eliminated global items
    1.50 -
    1.51 -  const "()" -> "Product_Type.Unity"
    1.52 -  type "unit" -> "Product_Type.unit"
    1.53 +* HOL: got rid of some global declarations (potential INCOMPATIBILITY
    1.54 +for ML tools): const "()" renamed "Product_Type.Unity", type "unit"
    1.55 +renamed "Product_Type.unit";
    1.56  
    1.57  
    1.58  *** ZF ***