--- a/src/HOL/Set.thy Fri Jan 06 21:48:45 2012 +0100
+++ b/src/HOL/Set.thy Fri Jan 06 21:48:45 2012 +0100
@@ -431,6 +431,10 @@
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
@@ -522,6 +526,10 @@
lemma set_mp: "A \<subseteq> B ==> x:A ==> x:B"
by (rule subsetD)
+lemma subset_not_subset_eq [code]:
+ "A \<subset> B \<longleftrightarrow> A \<subseteq> B \<and> \<not> B \<subseteq> A"
+ by (fact less_le_not_le)
+
lemma eq_mem_trans: "a=b ==> b \<in> A ==> a \<in> A"
by simp
@@ -1829,6 +1837,10 @@
"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