NEWS
changeset 14700 2f885b7e5ba7
parent 14699 2c9b463044ec
child 14707 2d6350d7b9b7
     1.1 --- a/NEWS	Sat May 01 22:28:51 2004 +0200
     1.2 +++ b/NEWS	Mon May 03 23:22:17 2004 +0200
     1.3 @@ -19,6 +19,7 @@
     1.4  depend on the signature of the theory context being presently used for
     1.5  parsing/printing, see also isar-ref manual.
     1.6  
     1.7 +
     1.8  * Pure: improved indexed syntax and implicit structures.  First of
     1.9  all, indexed syntax provides a notational device for subscripted
    1.10  application, using the new syntax \<^bsub>term\<^esub> for arbitrary
    1.11 @@ -30,6 +31,17 @@
    1.12  * Pure: tuned internal renaming of symbolic identifiers -- attach
    1.13  primes instead of base 26 numbers.
    1.14  
    1.15 +*** HOL ***
    1.16 +
    1.17 +* Records:
    1.18 +   Reimplementation of records to avoid performance problems for
    1.19 +   type inference. Records are no longer composed of nested field types,
    1.20 +   but of nested extension types. Therefore the record type only grows
    1.21 +   linear in the number of extensions and not in the number of fields.
    1.22 +   The top-level (users) view on records is preserved. 
    1.23 +   Potential INCOMPATIBILITY only in strange cases, where the theory
    1.24 +   depends on the old record representation. The type generated for
    1.25 +   a record is called <record_name>_ext_type.    
    1.26  
    1.27  *** HOLCF ***
    1.28