src/HOL/Set.thy
changeset 2412 025e80ed698d
parent 2393 651fce76c86c
child 2684 9781d63ef063
equal deleted inserted replaced
2411:256dbda3df4f 2412:025e80ed698d
   107   "@Bex"        :: [pttrn, 'a set, bool] => bool      ("(3\\<exists> _\\<in>_./ _)" [0, 0, 10] 10)
   107   "@Bex"        :: [pttrn, 'a set, bool] => bool      ("(3\\<exists> _\\<in>_./ _)" [0, 0, 10] 10)
   108 
   108 
   109 syntax (symbols output)
   109 syntax (symbols output)
   110   "*Ball"       :: [pttrn, 'a set, bool] => bool      ("(3\\<forall> _\\<in>_./ _)" [0, 0, 10] 10)
   110   "*Ball"       :: [pttrn, 'a set, bool] => bool      ("(3\\<forall> _\\<in>_./ _)" [0, 0, 10] 10)
   111   "*Bex"        :: [pttrn, 'a set, bool] => bool      ("(3\\<exists> _\\<in>_./ _)" [0, 0, 10] 10)
   111   "*Bex"        :: [pttrn, 'a set, bool] => bool      ("(3\\<exists> _\\<in>_./ _)" [0, 0, 10] 10)
       
   112 
       
   113 translations
       
   114   "op \\<subseteq>" => "op <="
   112 
   115 
   113 
   116 
   114 
   117 
   115 (** Rules and definitions **)
   118 (** Rules and definitions **)
   116 
   119