fixed typing of UN/INT syntax
authornipkow
Mon Mar 09 12:24:01 2009 +0100 (2009-03-09)
changeset 303842f24531b2d3e
parent 30372 96d508968153
child 30385 8befa897bebb
fixed typing of UN/INT syntax
src/HOL/Docs/MainDoc.thy
src/HOL/SetInterval.thy
     1.1 --- a/src/HOL/Docs/MainDoc.thy	Mon Mar 09 09:38:36 2009 +0100
     1.2 +++ b/src/HOL/Docs/MainDoc.thy	Mon Mar 09 12:24:01 2009 +0100
     1.3 @@ -341,7 +341,7 @@
     1.4  \end{supertabular}
     1.5  
     1.6  
     1.7 -\section{Set\_Interval}
     1.8 +\section{SetInterval}
     1.9  
    1.10  \begin{supertabular}{@ {} l @ {~::~} l @ {}}
    1.11  @{const lessThan} & @{term_type_only lessThan "'a::ord \<Rightarrow> 'a set"}\\
     2.1 --- a/src/HOL/SetInterval.thy	Mon Mar 09 09:38:36 2009 +0100
     2.2 +++ b/src/HOL/SetInterval.thy	Mon Mar 09 12:24:01 2009 +0100
     2.3 @@ -54,22 +54,22 @@
     2.4  @{term"{m..<n}"} may not exist in @{term"{..<n}"}-form as well. *}
     2.5  
     2.6  syntax
     2.7 -  "@UNION_le"   :: "nat => nat => 'b set => 'b set"       ("(3UN _<=_./ _)" 10)
     2.8 -  "@UNION_less" :: "nat => nat => 'b set => 'b set"       ("(3UN _<_./ _)" 10)
     2.9 -  "@INTER_le"   :: "nat => nat => 'b set => 'b set"       ("(3INT _<=_./ _)" 10)
    2.10 -  "@INTER_less" :: "nat => nat => 'b set => 'b set"       ("(3INT _<_./ _)" 10)
    2.11 +  "@UNION_le"   :: "'a => 'a => 'b set => 'b set"       ("(3UN _<=_./ _)" 10)
    2.12 +  "@UNION_less" :: "'a => 'a => 'b set => 'b set"       ("(3UN _<_./ _)" 10)
    2.13 +  "@INTER_le"   :: "'a => 'a => 'b set => 'b set"       ("(3INT _<=_./ _)" 10)
    2.14 +  "@INTER_less" :: "'a => 'a => 'b set => 'b set"       ("(3INT _<_./ _)" 10)
    2.15  
    2.16  syntax (xsymbols)
    2.17 -  "@UNION_le"   :: "nat => nat => 'b set => 'b set"       ("(3\<Union> _\<le>_./ _)" 10)
    2.18 -  "@UNION_less" :: "nat => nat => 'b set => 'b set"       ("(3\<Union> _<_./ _)" 10)
    2.19 -  "@INTER_le"   :: "nat => nat => 'b set => 'b set"       ("(3\<Inter> _\<le>_./ _)" 10)
    2.20 -  "@INTER_less" :: "nat => nat => 'b set => 'b set"       ("(3\<Inter> _<_./ _)" 10)
    2.21 +  "@UNION_le"   :: "'a => 'a => 'b set => 'b set"       ("(3\<Union> _\<le>_./ _)" 10)
    2.22 +  "@UNION_less" :: "'a => 'a => 'b set => 'b set"       ("(3\<Union> _<_./ _)" 10)
    2.23 +  "@INTER_le"   :: "'a => 'a => 'b set => 'b set"       ("(3\<Inter> _\<le>_./ _)" 10)
    2.24 +  "@INTER_less" :: "'a => 'a => 'b set => 'b set"       ("(3\<Inter> _<_./ _)" 10)
    2.25  
    2.26  syntax (latex output)
    2.27 -  "@UNION_le"   :: "nat \<Rightarrow> nat => 'b set => 'b set"       ("(3\<Union>(00_ \<le> _)/ _)" 10)
    2.28 -  "@UNION_less" :: "nat \<Rightarrow> nat => 'b set => 'b set"       ("(3\<Union>(00_ < _)/ _)" 10)
    2.29 -  "@INTER_le"   :: "nat \<Rightarrow> nat => 'b set => 'b set"       ("(3\<Inter>(00_ \<le> _)/ _)" 10)
    2.30 -  "@INTER_less" :: "nat \<Rightarrow> nat => 'b set => 'b set"       ("(3\<Inter>(00_ < _)/ _)" 10)
    2.31 +  "@UNION_le"   :: "'a \<Rightarrow> 'a => 'b set => 'b set"       ("(3\<Union>(00_ \<le> _)/ _)" 10)
    2.32 +  "@UNION_less" :: "'a \<Rightarrow> 'a => 'b set => 'b set"       ("(3\<Union>(00_ < _)/ _)" 10)
    2.33 +  "@INTER_le"   :: "'a \<Rightarrow> 'a => 'b set => 'b set"       ("(3\<Inter>(00_ \<le> _)/ _)" 10)
    2.34 +  "@INTER_less" :: "'a \<Rightarrow> 'a => 'b set => 'b set"       ("(3\<Inter>(00_ < _)/ _)" 10)
    2.35  
    2.36  translations
    2.37    "UN i<=n. A"  == "UN i:{..n}. A"