src/HOL/Complete_Lattice.thy
changeset 36364 0e2679025aeb
parent 35828 46cfc4b8112e
child 36635 080b755377c0
     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"