1.1 --- a/src/HOL/SetInterval.thy	Fri Jul 16 17:32:34 2004 +0200
     1.2 +++ b/src/HOL/SetInterval.thy	Fri Jul 16 17:33:12 2004 +0200
     1.3 @@ -549,7 +549,7 @@
     1.4    "_from_to_setsum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Sum>_ = _.._./ _)" [0,0,0,10] 10)
     1.5    "_from_upto_setsum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Sum>_ = _..<_./ _)" [0,0,0,10] 10)
     1.6    "_upto_setsum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Sum>_<_./ _)" [0,0,10] 10)
     1.7 -syntax (latex output)
     1.8 +syntax (latex_sum output)
     1.9    "_from_to_setsum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b"
    1.10   ("(3\<^raw:$\sum_{>_ = _\<^raw:}^{>_\<^raw:}$> _)" [0,0,0,10] 10)
    1.11    "_from_upto_setsum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b"
    1.12 @@ -563,15 +563,22 @@
    1.13    "\<Sum>i<n. t" == "setsum (\<lambda>i. t) {..<n}"
    1.14  
    1.15  text{* The above introduces some pretty alternative syntaxes for
    1.16 -summation over intervals as shown on the left-hand side:
    1.17 +summation over intervals:
    1.18  \begin{center}
    1.19  \begin{tabular}{lll}
    1.20 -Sets & Indexed & TeX\\
    1.21 -@{term[source]"\<Sum>x\<in>{a..b}. e"} & @{term[source]"\<Sum>x=a..b. e"} & @{term"\<Sum>x=a..b. e"}\\
    1.22 -@{term[source]"\<Sum>x\<in>{a..<b}. e"} & @{term[source]"\<Sum>x=a..<b. e"} & @{term"\<Sum>x=a..<b. e"}\\
    1.23 -@{term[source]"\<Sum>x\<in>{..<b}. e"} & @{term[source]"\<Sum>x<b. e"} & @{term"\<Sum>x<b. e"}
    1.24 +Old & New & \LaTeX\\
    1.25 +@{term[source]"\<Sum>x\<in>{a..b}. e"} & @{term"\<Sum>x=a..b. e"} & @{term[mode=latex_sum]"\<Sum>x=a..b. e"}\\
    1.26 +@{term[source]"\<Sum>x\<in>{a..<b}. e"} & @{term"\<Sum>x=a..<b. e"} & @{term[mode=latex_sum]"\<Sum>x=a..<b. e"}\\
    1.27 +@{term[source]"\<Sum>x\<in>{..<b}. e"} & @{term"\<Sum>x<b. e"} & @{term[mode=latex_sum]"\<Sum>x<b. e"}
    1.28  \end{tabular}
    1.29  \end{center}
    1.30 +The left column shows the term before introduction of the new syntax,
    1.31 +the middle column shows the new (default) syntax, and the right column
    1.32 +shows a special syntax. The latter is only meaningful for latex output
    1.33 +and has to be activated explicitly by setting the print mode to
    1.34 +\texttt{latex\_sum} (e.g.\ via \texttt{mode=latex\_sum} in
    1.35 +antiquotations). It is not the default \LaTeX\ output because it only
    1.36 +works well with italic-style formulae, not tt-style.
    1.37  
    1.38  Note that for uniformity on @{typ nat} it is better to use
    1.39  @{term"\<Sum>x::nat=0..<n. e"} rather than @{text"\<Sum>x<n. e"}: @{text setsum} may