--- 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