src/HOL/Set.thy
changeset 2372 a2999e19703b
parent 2368 d394336997cf
child 2388 d1f0505fc602
equal deleted inserted replaced
2371:c5dc6f8b385b 2372:a2999e19703b
    98   "@INTER"      :: [pttrn, 'a set, 'b set] => 'b set  ("(3\\<Inter> _\\<in>_./ _)" 10)
    98   "@INTER"      :: [pttrn, 'a set, 'b set] => 'b set  ("(3\\<Inter> _\\<in>_./ _)" 10)
    99   Union         :: (('a set) set) => 'a set           ("\\<Union> _" [90] 90)
    99   Union         :: (('a set) set) => 'a set           ("\\<Union> _" [90] 90)
   100   Inter         :: (('a set) set) => 'a set           ("\\<Inter> _" [90] 90)
   100   Inter         :: (('a set) set) => 'a set           ("\\<Inter> _" [90] 90)
   101   "@Ball"       :: [pttrn, 'a set, bool] => bool      ("(3\\<forall> _\\<in>_./ _)" [0, 0, 10] 10)
   101   "@Ball"       :: [pttrn, 'a set, bool] => bool      ("(3\\<forall> _\\<in>_./ _)" [0, 0, 10] 10)
   102   "@Bex"        :: [pttrn, 'a set, bool] => bool      ("(3\\<exists> _\\<in>_./ _)" [0, 0, 10] 10)
   102   "@Bex"        :: [pttrn, 'a set, bool] => bool      ("(3\\<exists> _\\<in>_./ _)" [0, 0, 10] 10)
       
   103 
       
   104 syntax (symbols output)
   103   "*Ball"       :: [pttrn, 'a set, bool] => bool      ("(3\\<forall> _\\<in>_./ _)" [0, 0, 10] 10)
   105   "*Ball"       :: [pttrn, 'a set, bool] => bool      ("(3\\<forall> _\\<in>_./ _)" [0, 0, 10] 10)
   104   "*Bex"        :: [pttrn, 'a set, bool] => bool      ("(3\\<exists> _\\<in>_./ _)" [0, 0, 10] 10)
   106   "*Bex"        :: [pttrn, 'a set, bool] => bool      ("(3\\<exists> _\\<in>_./ _)" [0, 0, 10] 10)
   105 
   107 
   106 
   108 
   107 
   109