NEWS
changeset 14709 d01983034ded
parent 14707 2d6350d7b9b7
child 14731 5670fc027a3b
     1.1 --- a/NEWS	Thu May 06 14:20:13 2004 +0200
     1.2 +++ b/NEWS	Thu May 06 20:43:30 2004 +0200
     1.3 @@ -34,15 +34,22 @@
     1.4  
     1.5  *** HOL ***
     1.6  
     1.7 -* HOL/record: reimplementation of records to avoid performance
     1.8 -problems for type inference. Records are no longer composed of nested
     1.9 -field types, but of nested extension types. Therefore the record type
    1.10 -only grows linear in the number of extensions and not in the number of
    1.11 -fields.  The top-level (users) view on records is preserved.
    1.12 +
    1.13 +* HOL/record: reimplementation of records. Improved scalability for records with
    1.14 +many fields, avoiding performance problems for type inference. Records are no 
    1.15 +longer composed of nested field types,
    1.16 +but of nested extension types. Therefore the record type only grows
    1.17 +linear in the number of extensions and not in the number of fields.
    1.18 +The top-level (users) view on records is preserved. 
    1.19  Potential INCOMPATIBILITY only in strange cases, where the theory
    1.20 -depends on the old record representation. The type generated for a
    1.21 -record is called <record_name>_ext_type.
    1.22 -
    1.23 +depends on the old record representation. The type generated for
    1.24 +a record is called <record_name>_ext_type.    
    1.25 +
    1.26 +
    1.27 +* Simplifier: "record_upd_simproc" for simplification of multiple record 
    1.28 +updates enabled by default. 
    1.29 +INCOMPATIBILITY: old proofs break occasionally, since simplification
    1.30 +is more powerful by default.
    1.31  
    1.32  *** HOLCF ***
    1.33