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

author | nipkow |

Thu, 22 Jul 2004 12:55:36 +0200 | |

changeset 15073 | 279c2daaf517 |

parent 15072 | 4861bf6af0b4 |

child 15074 | 277b3a4da341 |

*** empty log message ***

--- a/NEWS Thu Jul 22 10:33:26 2004 +0200 +++ b/NEWS Thu Jul 22 12:55:36 2004 +0200 @@ -169,7 +169,12 @@ They are not perfect but work quite well. -* HOL: There is new syntax for summation over finite sets: +* HOL: The syntax for 'setsum', summation over finite sets, has changed: + + The syntax for 'setsum (%x. e) A' used to be '\<Sum>x:A. e' + and is now either 'SUM x:A. e' or '\<Sum>x\<in>A. e'. + + There is new syntax for summation over finite sets: '\<Sum>x | P. e' is the same as 'setsum (%x. e) {x. P}' '\<Sum>x=a..b. e' is the same as 'setsum (%x. e) {a..b}'