1.1 --- a/NEWS	Wed May 12 11:08:15 2010 +0200
     1.2 +++ b/NEWS	Wed May 12 11:13:33 2010 +0200
     1.3 @@ -149,7 +149,8 @@
     1.4  * Dropped theorem RealPow.real_sq_order; use power2_le_imp_le instead.
     1.5  INCOMPATIBILITY.
     1.6  
     1.7 -* Dropped normalizing. Use semiring classes directly. INCOMPATIBILITY.
     1.8 +* Dropped normalizing_semiring etc; use the facts in semiring classes instead.
     1.9 +INCOMPATIBILITY.
    1.10  
    1.11  * Theory 'Finite_Set': various folding_* locales facilitate the application
    1.12  of the various fold combinators on finite sets.