1.1 --- a/NEWS	Thu Oct 25 02:12:10 2001 +0200
     1.2 +++ b/NEWS	Thu Oct 25 02:13:02 2001 +0200
     1.3 @@ -97,6 +97,14 @@
     1.4  
     1.5    - remove all special provisions on numerals in proofs;
     1.6  
     1.7 +* HOL/record:
     1.8 +  - provides cases/induct rules for use with corresponding Isar methods;
     1.9 +  - "record" operation truncates to particular fixed record (acts like
    1.10 +    a type cast);
    1.11 +  - make_defs no longer part of default simps;
    1.12 +  - internal definitions directly based on a light-weight abstract
    1.13 +    theory of product types over typedef rather than datatype;
    1.14 +
    1.15  * HOL: concrete setsum syntax "\<Sum>i:A. b" == "setsum (%i. b) A"
    1.16  (beware of argument permutation!);
    1.17