src/HOL/Set.thy
changeset 2965 afbda7e26f15
parent 2912 3fac3e8d5d3e
child 3222 726a9b069947
equal deleted inserted replaced
2964:557a11310988 2965:afbda7e26f15
   111 syntax (symbols output)
   111 syntax (symbols output)
   112   "*Ball"       :: [pttrn, 'a set, bool] => bool      ("(3\\<forall> _\\<in>_./ _)" [0, 0, 10] 10)
   112   "*Ball"       :: [pttrn, 'a set, bool] => bool      ("(3\\<forall> _\\<in>_./ _)" [0, 0, 10] 10)
   113   "*Bex"        :: [pttrn, 'a set, bool] => bool      ("(3\\<exists> _\\<in>_./ _)" [0, 0, 10] 10)
   113   "*Bex"        :: [pttrn, 'a set, bool] => bool      ("(3\\<exists> _\\<in>_./ _)" [0, 0, 10] 10)
   114 
   114 
   115 translations
   115 translations
   116   "op \\<subseteq>" => "op <="
   116   "op \\<subseteq>" => "op <= :: [_ set, _ set] => bool"
   117   "op \\<subset>" => "op <"
   117   "op \\<subset>" => "op <  :: [_ set, _ set] => bool"
   118 
   118 
   119 
   119 
   120 
   120 
   121 (** Rules and definitions **)
   121 (** Rules and definitions **)
   122 
   122