--- a/NEWS Tue Jun 05 15:16:11 2007 +0200
+++ b/NEWS Tue Jun 05 15:17:02 2007 +0200
@@ -738,8 +738,7 @@
* Renamed constants "0" to "HOL.zero_class.zero" and "1" to "HOL.one_class.one".
INCOMPATIBILITY.
-* Added theory Code_Generator providing class 'eq', allowing for code
-generation with polymorphic equality.
+* Added class "HOL.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 --
@@ -952,6 +951,8 @@
*** ML ***
+* Generic arithmetic modules: Tools/integer.ML, Tools/rat.ML, Tools/float.ML
+
* Context data interfaces (Theory/Proof/GenericDataFun): removed
name/print, uninitialized data defaults to ad-hoc copy of empty value,
init only required for impure data. INCOMPATIBILITY: empty really