UN syntax fix
authornipkow
Mon Mar 09 09:38:36 2009 +0100 (2009-03-09)
changeset 3037296d508968153
parent 30371 b3a60d828de0
child 30373 ffdd7a1f1ff0
child 30384 2f24531b2d3e
UN syntax fix
src/HOL/Docs/MainDoc.thy
src/HOL/SetInterval.thy
     1.1 --- a/src/HOL/Docs/MainDoc.thy	Mon Mar 09 09:24:50 2009 +0100
     1.2 +++ b/src/HOL/Docs/MainDoc.thy	Mon Mar 09 09:38:36 2009 +0100
     1.3 @@ -370,6 +370,7 @@
     1.4  \multicolumn{2}{@ {}l@ {}}{Similarly for @{text"\<Inter>"} instead of @{text"\<Union>"}}\\
     1.5  @{term "setsum (%x. t) {a..b}"} & @{term[source] "setsum (\<lambda>x. t) {a..b}"}\\
     1.6  @{term "setsum (%x. t) {a..<b}"} & @{term[source] "setsum (\<lambda>x. t) {a..<b}"}\\
     1.7 +\multicolumn{2}{@ {}l@ {}}{Similarly for @{text"\<Prod>"} instead of @{text"\<Sum>"}}\\
     1.8  \end{supertabular}
     1.9  
    1.10  ???????
     2.1 --- a/src/HOL/SetInterval.thy	Mon Mar 09 09:24:50 2009 +0100
     2.2 +++ b/src/HOL/SetInterval.thy	Mon Mar 09 09:38:36 2009 +0100
     2.3 @@ -59,13 +59,13 @@
     2.4    "@INTER_le"   :: "nat => nat => 'b set => 'b set"       ("(3INT _<=_./ _)" 10)
     2.5    "@INTER_less" :: "nat => nat => 'b set => 'b set"       ("(3INT _<_./ _)" 10)
     2.6  
     2.7 -syntax (input)
     2.8 +syntax (xsymbols)
     2.9    "@UNION_le"   :: "nat => nat => 'b set => 'b set"       ("(3\<Union> _\<le>_./ _)" 10)
    2.10    "@UNION_less" :: "nat => nat => 'b set => 'b set"       ("(3\<Union> _<_./ _)" 10)
    2.11    "@INTER_le"   :: "nat => nat => 'b set => 'b set"       ("(3\<Inter> _\<le>_./ _)" 10)
    2.12    "@INTER_less" :: "nat => nat => 'b set => 'b set"       ("(3\<Inter> _<_./ _)" 10)
    2.13  
    2.14 -syntax (xsymbols)
    2.15 +syntax (latex output)
    2.16    "@UNION_le"   :: "nat \<Rightarrow> nat => 'b set => 'b set"       ("(3\<Union>(00_ \<le> _)/ _)" 10)
    2.17    "@UNION_less" :: "nat \<Rightarrow> nat => 'b set => 'b set"       ("(3\<Union>(00_ < _)/ _)" 10)
    2.18    "@INTER_le"   :: "nat \<Rightarrow> nat => 'b set => 'b set"       ("(3\<Inter>(00_ \<le> _)/ _)" 10)