HOL/record;
authorwenzelm
Wed Jan 14 11:21:35 1998 +0100 (1998-01-14)
changeset 4575e59cf7d816fe
parent 4574 b922012cc142
child 4576 be6b5edbca9f
HOL/record;
NEWS
     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