# HG changeset patch
# User haftmann
# Date 1158672692 -7200
# Node ID 926a76a84e9731a0da6bb6cea1f24cc9540480ba
# Parent  fd9b0b78a7d3810819d8946cdb8ebacaa1981f51
Operational Equality

diff -r fd9b0b78a7d3 -r 926a76a84e97 NEWS
--- a/NEWS	Tue Sep 19 15:31:25 2006 +0200
+++ b/NEWS	Tue Sep 19 15:31:32 2006 +0200
@@ -468,6 +468,9 @@
 
 *** HOL ***
 
+* New theory OperationalEquality providing class 'eq' with constant 'eq',
+allowing for code generation with polymorphic equality.
+
 * Numeral syntax: type 'bin' which was a mere type copy of 'int' has been
 abandoned in favour of plain 'int'. INCOMPATIBILITY -- Significant changes
 for setting up numeral syntax for types:
@@ -602,6 +605,10 @@
 
 *** ML ***
 
+* Pure/General/susp.ML:
+
+New module for delayed evaluations.
+
 * Pure/library:
 
 Semantically identical functions "equal_list" and "eq_list" have been