changeset 17189 b15f8e094874
parent 17172 f048bd26ed3a
child 17193 83708f724822
--- a/NEWS	Mon Aug 29 16:51:39 2005 +0200
+++ b/NEWS	Tue Aug 30 12:47:53 2005 +0200
@@ -19,7 +19,7 @@
 will disappear in the next release.  Use isatool fixheaders to convert
 existing theory files.  Note that there is no change in ancient
-non-Isar theories.
+non-Isar theories now, but these are likely to disappear soon.
 * Theory loader: parent theories can now also be referred to via
 relative and absolute paths.
@@ -315,7 +315,8 @@
 * theory Finite_Set: changed the syntax for 'setsum', summation over
 finite sets: "setsum (%x. e) A", which used to be "\<Sum>x:A. e", is
-now either "SUM x:A. e" or "\<Sum>x \<in> A. e".
+now either "SUM x:A. e" or "\<Sum>x \<in> A. e". The bound variable can 
+be a tuple pattern.
 Some new syntax forms are available: