# HG changeset patch
# User wenzelm
# Date 1126729135 -7200
# Node ID b4743198b939553f4d022d6b3e22972ff5b6fe3d
# Parent  495c799df31d88b8cc6fb2bc7fa743db3dcda49e
Method comm_ring for proving equalities in commutative rings.

diff -r 495c799df31d -r b4743198b939 NEWS
--- a/NEWS	Wed Sep 14 22:08:08 2005 +0200
+++ b/NEWS	Wed Sep 14 22:18:55 2005 +0200
@@ -344,7 +344,9 @@
   {)\([^\.]*\)\.\.  ->  {\1<\.\.}
   \.\.\([^(}]*\)(}  ->  \.\.<\1}
 
-* theory Finite_Set: changed the syntax for 'setsum', summation over
+* Method comm_ring for proving equalities in commutative rings.
+
+* Theory Finite_Set: changed the syntax for 'setsum', summation over
 finite sets: "setsum (%x. e) A", which used to be "\<Sum>x:A. e", is
 now either "SUM x:A. e" or "\<Sum>x \<in> A. e". The bound variable can
 be a tuple pattern.