--- a/src/HOL/Set.thy Sat Jan 07 20:18:56 2012 +0100
+++ b/src/HOL/Set.thy Sat Jan 07 20:44:23 2012 +0100
@@ -431,10 +431,6 @@
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
@@ -1837,10 +1833,6 @@
"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