# HG changeset patch
# User krauss
# Date 1335209512 -7200
# Node ID 400fccb77ec80398bd99129986a8092b6c61711f
# Parent  27a04da9c6e65909e318ee27639f91aad54269ba
NEWS

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