1.1 --- a/NEWS	Mon Apr 23 18:42:05 2012 +0200
     1.2 +++ b/NEWS	Mon Apr 23 21:31:52 2012 +0200
     1.3 @@ -358,6 +358,12 @@
     1.4  * Discontinued configuration option "syntax_positions": atomic terms
     1.5  in parse trees are always annotated by position constraints.
     1.6  
     1.7 +* HOL/Library/Set_Algebras.thy: Addition and multiplication on sets
     1.8 +are expressed via type classes again. The special syntax
     1.9 +\<oplus>/\<otimes> has been replaced by plain +/*. Removed constant
    1.10 +setsum_set, which is now subsumed by Big_Operators.setsum.
    1.11 +INCOMPATIBILITY.
    1.12 +
    1.13  * New theory HOL/Library/DAList provides an abstract type for
    1.14  association lists with distinct keys.
    1.15