src/HOL/SetInterval.thy
changeset 28853 69eb69659bf3
parent 28068 f6b2d1995171
child 29667 53103fc8ffa3
     1.1 --- a/src/HOL/SetInterval.thy	Wed Nov 19 17:04:29 2008 +0100
     1.2 +++ b/src/HOL/SetInterval.thy	Wed Nov 19 17:54:55 2008 +0100
     1.3 @@ -724,10 +724,10 @@
     1.4   ("(3\<^raw:$\sum_{>_ \<le> _\<^raw:}$> _)" [0,0,10] 10)
     1.5  
     1.6  translations
     1.7 -  "\<Sum>x=a..b. t" == "setsum (%x. t) {a..b}"
     1.8 -  "\<Sum>x=a..<b. t" == "setsum (%x. t) {a..<b}"
     1.9 -  "\<Sum>i\<le>n. t" == "setsum (\<lambda>i. t) {..n}"
    1.10 -  "\<Sum>i<n. t" == "setsum (\<lambda>i. t) {..<n}"
    1.11 +  "\<Sum>x=a..b. t" == "CONST setsum (%x. t) {a..b}"
    1.12 +  "\<Sum>x=a..<b. t" == "CONST setsum (%x. t) {a..<b}"
    1.13 +  "\<Sum>i\<le>n. t" == "CONST setsum (\<lambda>i. t) {..n}"
    1.14 +  "\<Sum>i<n. t" == "CONST setsum (\<lambda>i. t) {..<n}"
    1.15  
    1.16  text{* The above introduces some pretty alternative syntaxes for
    1.17  summation over intervals: