--- a/NEWS Sat May 01 22:28:51 2004 +0200
+++ b/NEWS Mon May 03 23:22:17 2004 +0200
@@ -19,6 +19,7 @@
depend on the signature of the theory context being presently used for
parsing/printing, see also isar-ref manual.
+
* Pure: improved indexed syntax and implicit structures. First of
all, indexed syntax provides a notational device for subscripted
application, using the new syntax \<^bsub>term\<^esub> for arbitrary
@@ -30,6 +31,17 @@
* Pure: tuned internal renaming of symbolic identifiers -- attach
primes instead of base 26 numbers.
+*** HOL ***
+
+* Records:
+ Reimplementation of records to avoid performance problems for
+ type inference. Records are no longer composed of nested field types,
+ but of nested extension types. Therefore the record type only grows
+ linear in the number of extensions and not in the number of fields.
+ The top-level (users) view on records is preserved.
+ Potential INCOMPATIBILITY only in strange cases, where the theory
+ depends on the old record representation. The type generated for
+ a record is called <record_name>_ext_type.
*** HOLCF ***