--- a/src/HOL/SetInterval.thy Wed Nov 19 17:04:29 2008 +0100
+++ b/src/HOL/SetInterval.thy Wed Nov 19 17:54:55 2008 +0100
@@ -724,10 +724,10 @@
("(3\<^raw:$\sum_{>_ \<le> _\<^raw:}$> _)" [0,0,10] 10)
translations
- "\<Sum>x=a..b. t" == "setsum (%x. t) {a..b}"
- "\<Sum>x=a..<b. t" == "setsum (%x. t) {a..<b}"
- "\<Sum>i\<le>n. t" == "setsum (\<lambda>i. t) {..n}"
- "\<Sum>i<n. t" == "setsum (\<lambda>i. t) {..<n}"
+ "\<Sum>x=a..b. t" == "CONST setsum (%x. t) {a..b}"
+ "\<Sum>x=a..<b. t" == "CONST setsum (%x. t) {a..<b}"
+ "\<Sum>i\<le>n. t" == "CONST setsum (\<lambda>i. t) {..n}"
+ "\<Sum>i<n. t" == "CONST setsum (\<lambda>i. t) {..<n}"
text{* The above introduces some pretty alternative syntaxes for
summation over intervals: