* HOL: concrete setsum syntax "\<Sum>i:A. b" == "setsum (%i. b) A"
authorwenzelm
Tue Oct 16 17:51:12 2001 +0200 (2001-10-16)
changeset 118021d5f5d2427d2
parent 11801 9505bd5e9a36
child 11803 30f2104953a1
* HOL: concrete setsum syntax "\<Sum>i:A. b" == "setsum (%i. b) A"
(beware of argument permutation!);
NEWS
     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"