# HG changeset patch
# User nipkow
# Date 1335210412 -7200
# Node ID 918e98008d6e0133b61469a53ca2136936d4c291
# Parent  400fccb77ec80398bd99129986a8092b6c61711f# Parent  8b4cd98f944eb2efb96f1e6b3d84f238d57ea257
merged

diff -r 8b4cd98f944e -r 918e98008d6e NEWS
--- a/NEWS	Mon Apr 23 21:46:37 2012 +0200
+++ b/NEWS	Mon Apr 23 21:46: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.