--- a/NEWS Thu Jul 15 15:39:51 2004 +0200
+++ b/NEWS Thu Jul 15 15:47:39 2004 +0200
@@ -171,8 +171,10 @@
* HOL: There is new syntax for summation over finite sets:
- '\<Sum>x | P. e' is the same as 'setsum (%x. e) {x. P}'
- '\<Sum>x<k. e' is the same as 'setsum (%x. e) {..<k}'
+ '\<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}'
+ '\<Sum>x=a..<b. e' is the same as 'setsum (%x. e) {a..<b}'
+ '\<Sum>x<k. e' is the same as 'setsum (%x. e) {..<k}'
Function 'Summation' over nat is gone, its syntax '\<Sum>i<k. e'
now translates into 'setsum' as above.