--- a/NEWS Wed Nov 22 10:20:22 2006 +0100
+++ b/NEWS Wed Nov 22 10:21:17 2006 +0100
@@ -560,7 +560,7 @@
INCOMPATIBILITY: ML code directly refering to constant names may need adaption
This in general only affects hand-written proof tactics, simprocs and so on.
-* New theory Code_Generator providing class 'eq' with constant 'eq',
+* New theory Code_Generator providing class 'eq',
allowing for code generation with polymorphic equality.
* Numeral syntax: type 'bin' which was a mere type copy of 'int' has been