diff -r 7e6f334b294b -r 33e5b40ec4bb NEWS
--- a/NEWS	Wed May 12 11:08:15 2010 +0200
+++ b/NEWS	Wed May 12 11:13:33 2010 +0200
@@ -149,7 +149,8 @@
 * Dropped theorem RealPow.real_sq_order; use power2_le_imp_le instead.
 INCOMPATIBILITY.
 
-* Dropped normalizing. Use semiring classes directly. INCOMPATIBILITY.
+* Dropped normalizing_semiring etc; use the facts in semiring classes instead.
+INCOMPATIBILITY.
 
 * Theory 'Finite_Set': various folding_* locales facilitate the application
 of the various fold combinators on finite sets.