src/HOL/Set.thy
changeset 8148 5ef0b624aadb
parent 8005 b64d86018785
child 10106 1b63e30437ee
     1.1 --- a/src/HOL/Set.thy	Thu Jan 27 15:30:10 2000 +0100
     1.2 +++ b/src/HOL/Set.thy	Fri Jan 28 11:22:02 2000 +0100
     1.3 @@ -102,16 +102,16 @@
     1.4    "op :"        :: ['a, 'a set] => bool               ("(_/ \\<in> _)" [50, 51] 50)
     1.5    "op ~:"       :: ['a, 'a set] => bool               ("op \\<notin>")
     1.6    "op ~:"       :: ['a, 'a set] => bool               ("(_/ \\<notin> _)" [50, 51] 50)
     1.7 -  "UN "         :: [idts, bool] => bool               ("(3\\<Union> _./ _)" 10)
     1.8 -  "INT "        :: [idts, bool] => bool               ("(3\\<Inter> _./ _)" 10)
     1.9 -  "@UNION1"     :: [pttrn, 'b set] => 'b set          ("(3\\<Union> _./ _)" 10)
    1.10 -  "@INTER1"     :: [pttrn, 'b set] => 'b set          ("(3\\<Inter> _./ _)" 10)
    1.11 -  "@UNION"      :: [pttrn, 'a set, 'b set] => 'b set  ("(3\\<Union> _\\<in>_./ _)" 10)
    1.12 -  "@INTER"      :: [pttrn, 'a set, 'b set] => 'b set  ("(3\\<Inter> _\\<in>_./ _)" 10)
    1.13 -  Union         :: (('a set) set) => 'a set           ("\\<Union> _" [90] 90)
    1.14 -  Inter         :: (('a set) set) => 'a set           ("\\<Inter> _" [90] 90)
    1.15 -  "_Ball"       :: [pttrn, 'a set, bool] => bool      ("(3\\<forall> _\\<in>_./ _)" [0, 0, 10] 10)
    1.16 -  "_Bex"        :: [pttrn, 'a set, bool] => bool      ("(3\\<exists> _\\<in>_./ _)" [0, 0, 10] 10)
    1.17 +  "UN "         :: [idts, bool] => bool               ("(3\\<Union>_./ _)" 10)
    1.18 +  "INT "        :: [idts, bool] => bool               ("(3\\<Inter>_./ _)" 10)
    1.19 +  "@UNION1"     :: [pttrn, 'b set] => 'b set          ("(3\\<Union>_./ _)" 10)
    1.20 +  "@INTER1"     :: [pttrn, 'b set] => 'b set          ("(3\\<Inter>_./ _)" 10)
    1.21 +  "@UNION"      :: [pttrn, 'a set, 'b set] => 'b set  ("(3\\<Union>_\\<in>_./ _)" 10)
    1.22 +  "@INTER"      :: [pttrn, 'a set, 'b set] => 'b set  ("(3\\<Inter>_\\<in>_./ _)" 10)
    1.23 +  Union         :: (('a set) set) => 'a set           ("\\<Union>_" [90] 90)
    1.24 +  Inter         :: (('a set) set) => 'a set           ("\\<Inter>_" [90] 90)
    1.25 +  "_Ball"       :: [pttrn, 'a set, bool] => bool      ("(3\\<forall>_\\<in>_./ _)" [0, 0, 10] 10)
    1.26 +  "_Bex"        :: [pttrn, 'a set, bool] => bool      ("(3\\<exists>_\\<in>_./ _)" [0, 0, 10] 10)
    1.27  
    1.28  translations
    1.29    "op \\<subseteq>" => "op <= :: [_ set, _ set] => bool"