# HG changeset patch
# User nipkow
# Date 1089873517 -7200
# Node ID f224d27bb1f8caff9d8ec2d057dce52870b0c5d8
# Parent  b21fce6d146a4601e3d7e8c17175f33e305768d2
*** empty log message ***

diff -r b21fce6d146a -r f224d27bb1f8 NEWS
--- a/NEWS	Wed Jul 14 10:25:21 2004 +0200
+++ b/NEWS	Thu Jul 15 08:38:37 2004 +0200
@@ -152,6 +152,8 @@
   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'.
 
 *** HOLCF ***