src/HOL/Set.thy

   by blast
 
 lemma bex_triv_one_point2 [simp]: "(EX x:A. a = x) = (a:A)"
   by blast
 
-lemma member_exists [code]:
-  "a \<in> A \<longleftrightarrow> (\<exists>x\<in>A. a = x)"
-  by (rule sym) (fact bex_triv_one_point2)
-
 lemma bex_one_point1 [simp]: "(EX x:A. x = a & P x) = (a:A & P a)"
   by blast
 
 lemma bex_one_point2 [simp]: "(EX x:A. a = x & P x) = (a:A & P a)"
   by blast

 hide_const (open) project
 
 lemma member_project [simp]:
   "x \<in> Set.project P A \<longleftrightarrow> x \<in> A \<and> P x"
   by (simp add: project_def)
-
-lemma inter_project [code]:
-  "A \<inter> B = Set.project (\<lambda>x. x \<in> A) B"
-  by (auto simp add: project_def)
 
 instantiation set :: (equal) equal
 begin
 
 definition