src/HOL/Predicate_Compile.thy

   Introduce a new constant for membership to allow 
   fine-grained control in code equations. 
 \<close>
 
 definition contains :: "'a set => 'a => bool"
-where "contains A x \<longleftrightarrow> x : A"
+where "contains A x \<longleftrightarrow> x \<in> A"
 
 definition contains_pred :: "'a set => 'a => unit Predicate.pred"
-where "contains_pred A x = (if x : A then Predicate.single () else bot)"
+where "contains_pred A x = (if x \<in> A then Predicate.single () else bot)"
 
 lemma pred_of_setE:
   assumes "Predicate.eval (pred_of_set A) x"
   obtains "contains A x"
 using assms by(simp add: contains_def)

 
 lemma containsI: "x \<in> A ==> contains A x" 
 by(simp add: contains_def)
 
 lemma containsE: assumes "contains A x"
-  obtains A' x' where "A = A'" "x = x'" "x : A"
+  obtains A' x' where "A = A'" "x = x'" "x \<in> A"
 using assms by(simp add: contains_def)
 
 lemma contains_predI: "contains A x ==> Predicate.eval (contains_pred A x) ()"
 by(simp add: contains_pred_def contains_def)