# HG changeset patch
# User wenzelm
# Date 884773295 -3600
# Node ID e59cf7d816fe59f81eb90a155dd0b9f74c458b3f
# Parent  b922012cc142e966b2903bbf711c2343f2b8893f
HOL/record;

diff -r b922012cc142 -r e59cf7d816fe NEWS
--- a/NEWS	Wed Jan 14 11:10:19 1998 +0100
+++ b/NEWS	Wed Jan 14 11:21:35 1998 +0100
@@ -192,6 +192,10 @@
 * HOL/Set: The operator (UN x.B x) now abbreviates (UN x:UNIV. B x) and its
   specialist theorems (like UN1_I) are gone.  Similarly for (INT x.B x);
 
+* HOL/record: extensible records with schematic structural subtyping
+(single inheritance); EXPERIMENTAL version demonstrating the encoding,
+still lacks various theorems and concrete record syntax;
+
 
 *** HOLCF ***