* HOL/record:
authorwenzelm
Thu Oct 25 02:13:02 2001 +0200 (2001-10-25)
changeset 119301accec985349
parent 11929 a77ad6c86564
child 11931 a5d1c9b34900
* 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;
- internal definitions directly based on a light-weight abstract
theory of product types over typedef rather than datatype;
NEWS
     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