--- a/src/HOL/Docs/MainDoc.thy Mon Mar 09 09:24:50 2009 +0100
+++ b/src/HOL/Docs/MainDoc.thy Mon Mar 09 09:38:36 2009 +0100
@@ -370,6 +370,7 @@
\multicolumn{2}{@ {}l@ {}}{Similarly for @{text"\<Inter>"} instead of @{text"\<Union>"}}\\
@{term "setsum (%x. t) {a..b}"} & @{term[source] "setsum (\<lambda>x. t) {a..b}"}\\
@{term "setsum (%x. t) {a..<b}"} & @{term[source] "setsum (\<lambda>x. t) {a..<b}"}\\
+\multicolumn{2}{@ {}l@ {}}{Similarly for @{text"\<Prod>"} instead of @{text"\<Sum>"}}\\
\end{supertabular}
???????
--- a/src/HOL/SetInterval.thy Mon Mar 09 09:24:50 2009 +0100
+++ b/src/HOL/SetInterval.thy Mon Mar 09 09:38:36 2009 +0100
@@ -59,13 +59,13 @@
"@INTER_le" :: "nat => nat => 'b set => 'b set" ("(3INT _<=_./ _)" 10)
"@INTER_less" :: "nat => nat => 'b set => 'b set" ("(3INT _<_./ _)" 10)
-syntax (input)
+syntax (xsymbols)
"@UNION_le" :: "nat => nat => 'b set => 'b set" ("(3\<Union> _\<le>_./ _)" 10)
"@UNION_less" :: "nat => nat => 'b set => 'b set" ("(3\<Union> _<_./ _)" 10)
"@INTER_le" :: "nat => nat => 'b set => 'b set" ("(3\<Inter> _\<le>_./ _)" 10)
"@INTER_less" :: "nat => nat => 'b set => 'b set" ("(3\<Inter> _<_./ _)" 10)
-syntax (xsymbols)
+syntax (latex output)
"@UNION_le" :: "nat \<Rightarrow> nat => 'b set => 'b set" ("(3\<Union>(00_ \<le> _)/ _)" 10)
"@UNION_less" :: "nat \<Rightarrow> nat => 'b set => 'b set" ("(3\<Union>(00_ < _)/ _)" 10)
"@INTER_le" :: "nat \<Rightarrow> nat => 'b set => 'b set" ("(3\<Inter>(00_ \<le> _)/ _)" 10)