src/HOL/Set.thy

   mem_Collect_eq [iff, code_unfold]: "member a (Collect P) = P a"
   and Collect_mem_eq [simp]: "Collect (\<lambda>x. member x A) = A"
 
 notation
   member  ("op :") and
-  member  ("(_/ : _)" [50, 51] 50)
+  member  ("(_/ : _)" [51, 51] 50)
 
 abbreviation not_member where
   "not_member x A \<equiv> ~ (x : A)" -- "non-membership"
 
 notation
   not_member  ("op ~:") and
-  not_member  ("(_/ ~: _)" [50, 51] 50)
+  not_member  ("(_/ ~: _)" [51, 51] 50)
 
 notation (xsymbols)
   member      ("op \<in>") and
-  member      ("(_/ \<in> _)" [50, 51] 50) and
+  member      ("(_/ \<in> _)" [51, 51] 50) and
   not_member  ("op \<notin>") and
-  not_member  ("(_/ \<notin> _)" [50, 51] 50)
+  not_member  ("(_/ \<notin> _)" [51, 51] 50)
 
 notation (HTML output)
   member      ("op \<in>") and
-  member      ("(_/ \<in> _)" [50, 51] 50) and
+  member      ("(_/ \<in> _)" [51, 51] 50) and
   not_member  ("op \<notin>") and
-  not_member  ("(_/ \<notin> _)" [50, 51] 50)
+  not_member  ("(_/ \<notin> _)" [51, 51] 50)
 
 
 text {* Set comprehensions *}
 
 syntax

   subset_eq :: "'a set \<Rightarrow> 'a set \<Rightarrow> bool" where
   "subset_eq \<equiv> less_eq"
 
 notation (output)
   subset  ("op <") and
-  subset  ("(_/ < _)" [50, 51] 50) and
+  subset  ("(_/ < _)" [51, 51] 50) and
   subset_eq  ("op <=") and
-  subset_eq  ("(_/ <= _)" [50, 51] 50)
+  subset_eq  ("(_/ <= _)" [51, 51] 50)
 
 notation (xsymbols)
   subset  ("op \<subset>") and
-  subset  ("(_/ \<subset> _)" [50, 51] 50) and
+  subset  ("(_/ \<subset> _)" [51, 51] 50) and
   subset_eq  ("op \<subseteq>") and
-  subset_eq  ("(_/ \<subseteq> _)" [50, 51] 50)
+  subset_eq  ("(_/ \<subseteq> _)" [51, 51] 50)
 
 notation (HTML output)
   subset  ("op \<subset>") and
-  subset  ("(_/ \<subset> _)" [50, 51] 50) and
+  subset  ("(_/ \<subset> _)" [51, 51] 50) and
   subset_eq  ("op \<subseteq>") and
-  subset_eq  ("(_/ \<subseteq> _)" [50, 51] 50)
+  subset_eq  ("(_/ \<subseteq> _)" [51, 51] 50)
 
 abbreviation (input)
   supset :: "'a set \<Rightarrow> 'a set \<Rightarrow> bool" where
   "supset \<equiv> greater"
 

   supset_eq :: "'a set \<Rightarrow> 'a set \<Rightarrow> bool" where
   "supset_eq \<equiv> greater_eq"
 
 notation (xsymbols)
   supset  ("op \<supset>") and
-  supset  ("(_/ \<supset> _)" [50, 51] 50) and
+  supset  ("(_/ \<supset> _)" [51, 51] 50) and
   supset_eq  ("op \<supseteq>") and
-  supset_eq  ("(_/ \<supseteq> _)" [50, 51] 50)
+  supset_eq  ("(_/ \<supseteq> _)" [51, 51] 50)
 
 definition Ball :: "'a set \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> bool" where
   "Ball A P \<longleftrightarrow> (\<forall>x. x \<in> A \<longrightarrow> P x)"   -- "bounded universal quantifiers"
 
 definition Bex :: "'a set \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> bool" where