# HG changeset patch
# User nipkow
# Date 1089899259 -7200
# Node ID e02f678887bb4497df2a7d1759b928a46076b632
# Parent  82fb871517186efa953b7ae0ca112b9f343c2926
*** empty log message ***

diff -r 82fb87151718 -r e02f678887bb NEWS
--- 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.