NEWS
changeset 4575 e59cf7d816fe
parent 4502 337c073de95e
child 4649 89ad3eb863a1
     1.1 --- a/NEWS	Wed Jan 14 11:10:19 1998 +0100
     1.2 +++ b/NEWS	Wed Jan 14 11:21:35 1998 +0100
     1.3 @@ -192,6 +192,10 @@
     1.4  * HOL/Set: The operator (UN x.B x) now abbreviates (UN x:UNIV. B x) and its
     1.5    specialist theorems (like UN1_I) are gone.  Similarly for (INT x.B x);
     1.6  
     1.7 +* HOL/record: extensible records with schematic structural subtyping
     1.8 +(single inheritance); EXPERIMENTAL version demonstrating the encoding,
     1.9 +still lacks various theorems and concrete record syntax;
    1.10 +
    1.11  
    1.12  *** HOLCF ***
    1.13