src/HOL/Set.thy
changeset 10106 1b63e30437ee
parent 8148 5ef0b624aadb
child 10131 546686f0a6fb
     1.1 --- a/src/HOL/Set.thy	Thu Sep 28 14:41:48 2000 +0200
     1.2 +++ b/src/HOL/Set.thy	Thu Sep 28 14:42:21 2000 +0200
     1.3 @@ -56,9 +56,8 @@
     1.4  
     1.5    (* Big Intersection / Union *)
     1.6  
     1.7 -  "@INTER1"     :: [pttrns, 'b set] => 'b set   ("(3INT _./ _)" 10)
     1.8 -  "@UNION1"     :: [pttrns, 'b set] => 'b set   ("(3UN _./ _)" 10)
     1.9 -
    1.10 +  "@INTER1"     :: [pttrns, 'b set] => 'b set         ("(3INT _./ _)" 10)
    1.11 +  "@UNION1"     :: [pttrns, 'b set] => 'b set         ("(3UN _./ _)" 10)
    1.12    "@INTER"      :: [pttrn, 'a set, 'b set] => 'b set  ("(3INT _:_./ _)" 10)
    1.13    "@UNION"      :: [pttrn, 'a set, 'b set] => 'b set  ("(3UN _:_./ _)" 10)
    1.14  
    1.15 @@ -102,10 +101,8 @@
    1.16    "op :"        :: ['a, 'a set] => bool               ("(_/ \\<in> _)" [50, 51] 50)
    1.17    "op ~:"       :: ['a, 'a set] => bool               ("op \\<notin>")
    1.18    "op ~:"       :: ['a, 'a set] => bool               ("(_/ \\<notin> _)" [50, 51] 50)
    1.19 -  "UN "         :: [idts, bool] => bool               ("(3\\<Union>_./ _)" 10)
    1.20 -  "INT "        :: [idts, bool] => bool               ("(3\\<Inter>_./ _)" 10)
    1.21 -  "@UNION1"     :: [pttrn, 'b set] => 'b set          ("(3\\<Union>_./ _)" 10)
    1.22 -  "@INTER1"     :: [pttrn, 'b set] => 'b set          ("(3\\<Inter>_./ _)" 10)
    1.23 +  "@UNION1"     :: [pttrns, 'b set] => 'b set         ("(3\\<Union>_./ _)" 10)
    1.24 +  "@INTER1"     :: [pttrns, 'b set] => 'b set         ("(3\\<Inter>_./ _)" 10)
    1.25    "@UNION"      :: [pttrn, 'a set, 'b set] => 'b set  ("(3\\<Union>_\\<in>_./ _)" 10)
    1.26    "@INTER"      :: [pttrn, 'a set, 'b set] => 'b set  ("(3\\<Inter>_\\<in>_./ _)" 10)
    1.27    Union         :: (('a set) set) => 'a set           ("\\<Union>_" [90] 90)