src/HOL/Set.thy

   and member :: "'a \<Rightarrow> 'a set \<Rightarrow> bool" \<comment> "membership"
   where 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  (infix "\<in>" 50)
+  member  ("'(\<in>')") and
+  member  ("(_/ \<in> _)" [51, 51] 50)
 
 abbreviation not_member
   where "not_member x A \<equiv> \<not> (x \<in> A)" \<comment> "non-membership"
 notation
-  not_member  (infix "\<notin>" 50)
+  not_member  ("'(\<notin>')") and
+  not_member  ("(_/ \<notin> _)" [51, 51] 50)
 
 notation (ASCII)
-  member  (infix ":" 50) and
-  not_member  (infix "~:" 50)
+  member  ("'(:')") and
+  member  ("(_/ : _)" [51, 51] 50) and
+  not_member  ("'(~:')") and
+  not_member  ("(_/ ~: _)" [51, 51] 50)
 
 
 text \<open>Set comprehensions\<close>
 
 syntax