--- a/NEWS Mon May 03 10:28:19 2010 -0700
+++ b/NEWS Tue May 04 08:55:34 2010 +0200
@@ -89,6 +89,9 @@
*** Pure ***
+* Predicates of locales introduces by classes carry a mandatory "class"
+prefix. INCOMPATIBILITY.
+
* 'code_reflect' allows to incorporate generated ML code into
runtime environment; replaces immature code_datatype antiquotation.
INCOMPATIBILITY.
@@ -137,6 +140,9 @@
*** HOL ***
+* Theory 'Finite_Set': various folding_* locales facilitate the application
+of the various fold combinators on finite sets.
+
* Library theory 'RBT' renamed to 'RBT_Impl'; new library theory 'RBT'
provides abstract red-black tree type which is backed by RBT_Impl
as implementation. INCOMPATIBILTY.