# HG changeset patch
# User nipkow
# Date 1089971219 -7200
# Node ID cc562a263609747562efcb545da0537a7ec1e465
# Parent  0dbbab9f77fe1a2f65c825b870ff16b1236f53b5
Added nice latex syntax.

diff -r 0dbbab9f77fe -r cc562a263609 src/HOL/SetInterval.thy
--- a/src/HOL/SetInterval.thy	Fri Jul 16 09:36:04 2004 +0200
+++ b/src/HOL/SetInterval.thy	Fri Jul 16 11:46:59 2004 +0200
@@ -53,7 +53,7 @@
 
 text{* A note of warning when using @{term"{..<n}"} on type @{typ
 nat}: it is equivalent to @{term"{0::nat..<n}"} but some lemmas involving
-@{term"{m..<n}"} may not exist for in @{term"{..<n}"}-form as well. *}
+@{term"{m..<n}"} may not exist in @{term"{..<n}"}-form as well. *}
 
 syntax
   "@UNION_le"   :: "nat => nat => 'b set => 'b set"       ("(3UN _<=_./ _)" 10)
@@ -537,15 +537,6 @@
 
 subsection {* Summation indexed over intervals *}
 
-text{* We introduce the obvious syntax @{text"\<Sum>x=a..b. e"} for
-@{term"\<Sum>x\<in>{a..b}. e"}, @{text"\<Sum>x=a..<b. e"} for
-@{term"\<Sum>x\<in>{a..<b}. e"}, and @{text"\<Sum>x<b. e"} for @{term"\<Sum>x\<in>{..<b}. e"}.
-
-Note that for uniformity on @{typ nat} it is better to use
-@{text"\<Sum>x=0..<n. e"} rather than @{text"\<Sum>x<n. e"}: @{text setsum} may
-not provide all lemmas available for @{term"{m..<n}"} also in the
-special form for @{term"{..<n}"}. *}
-
 syntax
   "_from_to_setsum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" ("(SUM _ = _.._./ _)" [0,0,0,10] 10)
   "_from_upto_setsum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" ("(SUM _ = _..<_./ _)" [0,0,0,10] 10)
@@ -558,12 +549,35 @@
   "_from_to_setsum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Sum>_ = _.._./ _)" [0,0,0,10] 10)
   "_from_upto_setsum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Sum>_ = _..<_./ _)" [0,0,0,10] 10)
   "_upto_setsum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Sum>_<_./ _)" [0,0,10] 10)
+syntax (latex output)
+  "_from_to_setsum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b"
+ ("(3\<^raw:$\sum_{>_ = _\<^raw:}^{>_\<^raw:}$> _)" [0,0,0,10] 10)
+  "_from_upto_setsum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b"
+ ("(3\<^raw:$\sum_{>_ = _\<^raw:}^{<>_\<^raw:}$> _)" [0,0,0,10] 10)
+  "_upto_setsum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b"
+ ("(3\<^raw:$\sum_{>_ < _\<^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<n. t" == "setsum (\<lambda>i. t) {..<n}"
 
+text{* The above introduces some pretty alternative syntaxes for
+summation over intervals as shown on the left-hand side:
+\begin{center}
+\begin{tabular}{lll}
+Sets & Indexed & TeX\\
+@{term[source]"\<Sum>x\<in>{a..b}. e"} & @{term[source]"\<Sum>x=a..b. e"} & @{term"\<Sum>x=a..b. e"}\\
+@{term[source]"\<Sum>x\<in>{a..<b}. e"} & @{term[source]"\<Sum>x=a..<b. e"} & @{term"\<Sum>x=a..<b. e"}\\
+@{term[source]"\<Sum>x\<in>{..<b}. e"} & @{term[source]"\<Sum>x<b. e"} & @{term"\<Sum>x<b. e"}
+\end{tabular}
+\end{center}
+
+Note that for uniformity on @{typ nat} it is better to use
+@{term"\<Sum>x::nat=0..<n. e"} rather than @{text"\<Sum>x<n. e"}: @{text setsum} may
+not provide all lemmas available for @{term"{m..<n}"} also in the
+special form for @{term"{..<n}"}. *}
+
 
 lemma Summation_Suc[simp]: "(\<Sum>i < Suc n. b i) = b n + (\<Sum>i < n. b i)"
 by (simp add:lessThan_Suc)