* HOL: concrete setsum syntax "\<Sum>i:A. b" == "setsum (%i. b) A"
(beware of argument permutation!);

--- a/NEWS	Tue Oct 16 17:25:44 2001 +0200
+++ b/NEWS	Tue Oct 16 17:51:12 2001 +0200
@@ -79,6 +79,9 @@
 
   - remove all special provisions on numerals in proofs;
 
+* HOL: concrete setsum syntax "\<Sum>i:A. b" == "setsum (%i. b) A"
+(beware of argument permutation!);
+
 * HOL: linorder_less_split superseded by linorder_cases;
 
 * HOL: added "The" definite description operator; move Hilbert's "Eps"