summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | wenzelm |

Wed, 14 Sep 2005 22:18:55 +0200 | |

changeset 17389 | b4743198b939 |

parent 17388 | 495c799df31d |

child 17390 | df2b53a66937 |

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.