1.1 --- a/NEWS	Thu Jan 06 17:51:56 2011 +0100
     1.2 +++ b/NEWS	Thu Jan 06 21:06:17 2011 +0100
     1.3 @@ -498,6 +498,14 @@
     1.4  INCOMPATIBILITY.
     1.5  
     1.6  
     1.7 +*** HOL-Algebra ***
     1.8 +
     1.9 +* Theorems for additive ring operations (locale abelian_monoid and
    1.10 +descendants) are generated by interpretation from their multiplicative
    1.11 +counterparts.  This causes slight differences in the simp and clasets.
    1.12 +INCOMPATIBILITY.
    1.13 +
    1.14 +
    1.15  *** HOLCF ***
    1.16  
    1.17  * The domain package now runs in definitional mode by default: The