Method comm_ring for proving equalities in commutative rings.

--- 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.