fix syntax precedence declarations for UNION, INTER, SUP, INF
authorhuffman
Mon Apr 26 09:37:46 2010 -0700 (2010-04-26)
changeset 363640e2679025aeb
parent 36363 ebaa558fc698
child 36365 18bf20d0c2df
fix syntax precedence declarations for UNION, INTER, SUP, INF
src/HOL/Complete_Lattice.thy
src/HOL/SetInterval.thy
     1.1 --- a/src/HOL/Complete_Lattice.thy	Mon Apr 26 09:26:31 2010 -0700
     1.2 +++ b/src/HOL/Complete_Lattice.thy	Mon Apr 26 09:37:46 2010 -0700
     1.3 @@ -98,9 +98,9 @@
     1.4  
     1.5  syntax
     1.6    "_SUP1"     :: "pttrns => 'b => 'b"           ("(3SUP _./ _)" [0, 10] 10)
     1.7 -  "_SUP"      :: "pttrn => 'a set => 'b => 'b"  ("(3SUP _:_./ _)" [0, 10] 10)
     1.8 +  "_SUP"      :: "pttrn => 'a set => 'b => 'b"  ("(3SUP _:_./ _)" [0, 0, 10] 10)
     1.9    "_INF1"     :: "pttrns => 'b => 'b"           ("(3INF _./ _)" [0, 10] 10)
    1.10 -  "_INF"      :: "pttrn => 'a set => 'b => 'b"  ("(3INF _:_./ _)" [0, 10] 10)
    1.11 +  "_INF"      :: "pttrn => 'a set => 'b => 'b"  ("(3INF _:_./ _)" [0, 0, 10] 10)
    1.12  
    1.13  translations
    1.14    "SUP x y. B"   == "SUP x. SUP y. B"
    1.15 @@ -295,15 +295,15 @@
    1.16  
    1.17  syntax
    1.18    "_UNION1"     :: "pttrns => 'b set => 'b set"           ("(3UN _./ _)" [0, 10] 10)
    1.19 -  "_UNION"      :: "pttrn => 'a set => 'b set => 'b set"  ("(3UN _:_./ _)" [0, 10] 10)
    1.20 +  "_UNION"      :: "pttrn => 'a set => 'b set => 'b set"  ("(3UN _:_./ _)" [0, 0, 10] 10)
    1.21  
    1.22  syntax (xsymbols)
    1.23    "_UNION1"     :: "pttrns => 'b set => 'b set"           ("(3\<Union>_./ _)" [0, 10] 10)
    1.24 -  "_UNION"      :: "pttrn => 'a set => 'b set => 'b set"  ("(3\<Union>_\<in>_./ _)" [0, 10] 10)
    1.25 +  "_UNION"      :: "pttrn => 'a set => 'b set => 'b set"  ("(3\<Union>_\<in>_./ _)" [0, 0, 10] 10)
    1.26  
    1.27  syntax (latex output)
    1.28    "_UNION1"     :: "pttrns => 'b set => 'b set"           ("(3\<Union>(00\<^bsub>_\<^esub>)/ _)" [0, 10] 10)
    1.29 -  "_UNION"      :: "pttrn => 'a set => 'b set => 'b set"  ("(3\<Union>(00\<^bsub>_\<in>_\<^esub>)/ _)" [0, 10] 10)
    1.30 +  "_UNION"      :: "pttrn => 'a set => 'b set => 'b set"  ("(3\<Union>(00\<^bsub>_\<in>_\<^esub>)/ _)" [0, 0, 10] 10)
    1.31  
    1.32  translations
    1.33    "UN x y. B"   == "UN x. UN y. B"
    1.34 @@ -531,15 +531,15 @@
    1.35  
    1.36  syntax
    1.37    "_INTER1"     :: "pttrns => 'b set => 'b set"           ("(3INT _./ _)" [0, 10] 10)
    1.38 -  "_INTER"      :: "pttrn => 'a set => 'b set => 'b set"  ("(3INT _:_./ _)" [0, 10] 10)
    1.39 +  "_INTER"      :: "pttrn => 'a set => 'b set => 'b set"  ("(3INT _:_./ _)" [0, 0, 10] 10)
    1.40  
    1.41  syntax (xsymbols)
    1.42    "_INTER1"     :: "pttrns => 'b set => 'b set"           ("(3\<Inter>_./ _)" [0, 10] 10)
    1.43 -  "_INTER"      :: "pttrn => 'a set => 'b set => 'b set"  ("(3\<Inter>_\<in>_./ _)" [0, 10] 10)
    1.44 +  "_INTER"      :: "pttrn => 'a set => 'b set => 'b set"  ("(3\<Inter>_\<in>_./ _)" [0, 0, 10] 10)
    1.45  
    1.46  syntax (latex output)
    1.47    "_INTER1"     :: "pttrns => 'b set => 'b set"           ("(3\<Inter>(00\<^bsub>_\<^esub>)/ _)" [0, 10] 10)
    1.48 -  "_INTER"      :: "pttrn => 'a set => 'b set => 'b set"  ("(3\<Inter>(00\<^bsub>_\<in>_\<^esub>)/ _)" [0, 10] 10)
    1.49 +  "_INTER"      :: "pttrn => 'a set => 'b set => 'b set"  ("(3\<Inter>(00\<^bsub>_\<in>_\<^esub>)/ _)" [0, 0, 10] 10)
    1.50  
    1.51  translations
    1.52    "INT x y. B"  == "INT x. INT y. B"
     2.1 --- a/src/HOL/SetInterval.thy	Mon Apr 26 09:26:31 2010 -0700
     2.2 +++ b/src/HOL/SetInterval.thy	Mon Apr 26 09:37:46 2010 -0700
     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"   :: "'a => 'a => 'b set => 'b set"       ("(3UN _<=_./ _)" 10)
     2.8 -  "_UNION_less" :: "'a => 'a => 'b set => 'b set"       ("(3UN _<_./ _)" 10)
     2.9 -  "_INTER_le"   :: "'a => 'a => 'b set => 'b set"       ("(3INT _<=_./ _)" 10)
    2.10 -  "_INTER_less" :: "'a => 'a => 'b set => 'b set"       ("(3INT _<_./ _)" 10)
    2.11 +  "_UNION_le"   :: "'a => 'a => 'b set => 'b set"       ("(3UN _<=_./ _)" [0, 0, 10] 10)
    2.12 +  "_UNION_less" :: "'a => 'a => 'b set => 'b set"       ("(3UN _<_./ _)" [0, 0, 10] 10)
    2.13 +  "_INTER_le"   :: "'a => 'a => 'b set => 'b set"       ("(3INT _<=_./ _)" [0, 0, 10] 10)
    2.14 +  "_INTER_less" :: "'a => 'a => 'b set => 'b set"       ("(3INT _<_./ _)" [0, 0, 10] 10)
    2.15  
    2.16  syntax (xsymbols)
    2.17 -  "_UNION_le"   :: "'a => 'a => 'b set => 'b set"       ("(3\<Union> _\<le>_./ _)" 10)
    2.18 -  "_UNION_less" :: "'a => 'a => 'b set => 'b set"       ("(3\<Union> _<_./ _)" 10)
    2.19 -  "_INTER_le"   :: "'a => 'a => 'b set => 'b set"       ("(3\<Inter> _\<le>_./ _)" 10)
    2.20 -  "_INTER_less" :: "'a => 'a => 'b set => 'b set"       ("(3\<Inter> _<_./ _)" 10)
    2.21 +  "_UNION_le"   :: "'a => 'a => 'b set => 'b set"       ("(3\<Union> _\<le>_./ _)" [0, 0, 10] 10)
    2.22 +  "_UNION_less" :: "'a => 'a => 'b set => 'b set"       ("(3\<Union> _<_./ _)" [0, 0, 10] 10)
    2.23 +  "_INTER_le"   :: "'a => 'a => 'b set => 'b set"       ("(3\<Inter> _\<le>_./ _)" [0, 0, 10] 10)
    2.24 +  "_INTER_less" :: "'a => 'a => 'b set => 'b set"       ("(3\<Inter> _<_./ _)" [0, 0, 10] 10)
    2.25  
    2.26  syntax (latex output)
    2.27 -  "_UNION_le"   :: "'a \<Rightarrow> 'a => 'b set => 'b set"       ("(3\<Union>(00_ \<le> _)/ _)" 10)
    2.28 -  "_UNION_less" :: "'a \<Rightarrow> 'a => 'b set => 'b set"       ("(3\<Union>(00_ < _)/ _)" 10)
    2.29 -  "_INTER_le"   :: "'a \<Rightarrow> 'a => 'b set => 'b set"       ("(3\<Inter>(00_ \<le> _)/ _)" 10)
    2.30 -  "_INTER_less" :: "'a \<Rightarrow> 'a => 'b set => 'b set"       ("(3\<Inter>(00_ < _)/ _)" 10)
    2.31 +  "_UNION_le"   :: "'a \<Rightarrow> 'a => 'b set => 'b set"       ("(3\<Union>(00_ \<le> _)/ _)" [0, 0, 10] 10)
    2.32 +  "_UNION_less" :: "'a \<Rightarrow> 'a => 'b set => 'b set"       ("(3\<Union>(00_ < _)/ _)" [0, 0, 10] 10)
    2.33 +  "_INTER_le"   :: "'a \<Rightarrow> 'a => 'b set => 'b set"       ("(3\<Inter>(00_ \<le> _)/ _)" [0, 0, 10] 10)
    2.34 +  "_INTER_less" :: "'a \<Rightarrow> 'a => 'b set => 'b set"       ("(3\<Inter>(00_ < _)/ _)" [0, 0, 10] 10)
    2.35  
    2.36  translations
    2.37    "UN i<=n. A"  == "UN i:{..n}. A"