# HG changeset patch
# User nipkow
# Date 1236587916 -3600
# Node ID 96d508968153b371ce8cbfe8cd9e0499fdd3df2a
# Parent  b3a60d828de0a67a7da9fcdbfdbeaaa26955bb3c
UN syntax fix

diff -r b3a60d828de0 -r 96d508968153 src/HOL/Docs/MainDoc.thy
--- 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}
 
 ???????
diff -r b3a60d828de0 -r 96d508968153 src/HOL/SetInterval.thy
--- 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)