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