# HG changeset patch
# User nipkow
# Date 1089890685 -7200
# Node ID d6a4c3992e9dfd85123182bcdc57003ec9f7b155
# Parent  d59f7e2e18d3ef81128b428a721fba05a258e0fd
*** empty log message ***

diff -r d59f7e2e18d3 -r d6a4c3992e9d NEWS
--- a/NEWS	Thu Jul 15 13:11:34 2004 +0200
+++ b/NEWS	Thu Jul 15 13:24:45 2004 +0200
@@ -152,8 +152,31 @@
   Moreover, the mathematically important symbolic identifier
   \<epsilon> becomes available as variable, constant etc.
 
-* HOL: Summation over nat with syntax '\<Sum>i<k. e' is now just a
-  translation into 'setsum'.
+* HOL/SetInterval: The syntax for open intervals has changed:
+
+  Old         New
+  {..n(}   -> {..<n}
+  {)n..}   -> {n<..}
+  {m..n(}  -> {m..<n}
+  {)m..n}  -> {m<..n}
+  {)m..n(} -> {m<..<n}
+
+  The old syntax is still supported but will disappear in the future.
+  For conversion use the following emacs search and replace patterns:
+
+  {)\([^\.]*\)\.\.  ->  {\1<\.\.}
+  \.\.\([^(}]*\)(}  ->  \.\.<\1}
+
+  They are not perfect but work quite well.
+
+* 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}'
+
+  Function 'Summation' over nat is gone, its syntax '\<Sum>i<k. e'
+  now translates into 'setsum' as above.
+
 
 *** HOLCF ***