NEWS
changeset 36849 33e5b40ec4bb
parent 36848 7e6f334b294b
child 36856 b343091e81d8
--- 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.