NEWS
changeset 11936 fef099613354
parent 11933 acfea249b03c
child 11937 2a2b1182a23b
     1.1 --- a/NEWS	Thu Oct 25 20:04:43 2001 +0200
     1.2 +++ b/NEWS	Thu Oct 25 22:41:07 2001 +0200
     1.3 @@ -58,6 +58,9 @@
     1.4  bound variables: "ALL x. P x --> Q x" (is "ALL x. _ --> ?C x")
     1.5  supersedes more cumbersome ... (is "ALL x. _ x --> ?C x");
     1.6  
     1.7 +* Provers: 'simplified' attribute may refer to explicit rules instead
     1.8 +of full simplifier context; 'iff' attribute handles conditional rules;
     1.9 +
    1.10  * HOL: 'typedef' now allows alternative names for Rep/Abs morphisms;
    1.11  
    1.12  * HOL: 'recdef' now fails on unfinished automated proofs, use
    1.13 @@ -98,8 +101,11 @@
    1.14  
    1.15  * HOL/record:
    1.16    - provides cases/induct rules for use with corresponding Isar methods;
    1.17 -  - "record" operation truncates to particular fixed record (type cast);
    1.18 -  - make_defs no longer part of default simps (INCOMPATIBILITY);
    1.19 +  - old "make" and "make_scheme" operation removed -- INCOMPATIBILITY;
    1.20 +  - new derived operations "make" (for adding fields of current
    1.21 +    record), "extend" to promote fixed record to record scheme, and
    1.22 +    "truncate" for the reverse; cf. theorems "derived_defs", which are
    1.23 +    *not* declared as simp by default;
    1.24    - internal definitions directly based on a light-weight abstract
    1.25      theory of product types over typedef rather than datatype;
    1.26