Method comm_ring for proving equalities in commutative rings.
authorwenzelm
Wed Sep 14 22:18:55 2005 +0200 (2005-09-14)
changeset 17389b4743198b939
parent 17388 495c799df31d
child 17390 df2b53a66937
Method comm_ring for proving equalities in commutative rings.
NEWS
     1.1 --- a/NEWS	Wed Sep 14 22:08:08 2005 +0200
     1.2 +++ b/NEWS	Wed Sep 14 22:18:55 2005 +0200
     1.3 @@ -344,7 +344,9 @@
     1.4    {)\([^\.]*\)\.\.  ->  {\1<\.\.}
     1.5    \.\.\([^(}]*\)(}  ->  \.\.<\1}
     1.6  
     1.7 -* theory Finite_Set: changed the syntax for 'setsum', summation over
     1.8 +* Method comm_ring for proving equalities in commutative rings.
     1.9 +
    1.10 +* Theory Finite_Set: changed the syntax for 'setsum', summation over
    1.11  finite sets: "setsum (%x. e) A", which used to be "\<Sum>x:A. e", is
    1.12  now either "SUM x:A. e" or "\<Sum>x \<in> A. e". The bound variable can
    1.13  be a tuple pattern.