# HG changeset patch
# User wenzelm
# Date 1003247472 -7200
# Node ID 1d5f5d2427d26a8c3c4458b74a81ed87c9e1e488
# Parent  9505bd5e9a3602c445196e68807e245a3ce3b174
* HOL: concrete setsum syntax "\<Sum>i:A. b" == "setsum (%i. b) A"
  (beware of argument permutation!);

diff -r 9505bd5e9a36 -r 1d5f5d2427d2 NEWS
--- 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"