1.1 --- a/src/HOL/Set.thy	Fri Jan 06 21:48:45 2012 +0100
     1.2 +++ b/src/HOL/Set.thy	Fri Jan 06 21:48:45 2012 +0100
     1.3 @@ -431,6 +431,10 @@
     1.4  lemma bex_triv_one_point2 [simp]: "(EX x:A. a = x) = (a:A)"
     1.5    by blast
     1.6  
     1.7 +lemma member_exists [code]:
     1.8 +  "a \<in> A \<longleftrightarrow> (\<exists>x\<in>A. a = x)"
     1.9 +  by (rule sym) (fact bex_triv_one_point2)
    1.10 +
    1.11  lemma bex_one_point1 [simp]: "(EX x:A. x = a & P x) = (a:A & P a)"
    1.12    by blast
    1.13  
    1.14 @@ -522,6 +526,10 @@
    1.15  lemma set_mp: "A \<subseteq> B ==> x:A ==> x:B"
    1.16    by (rule subsetD)
    1.17  
    1.18 +lemma subset_not_subset_eq [code]:
    1.19 +  "A \<subset> B \<longleftrightarrow> A \<subseteq> B \<and> \<not> B \<subseteq> A"
    1.20 +  by (fact less_le_not_le)
    1.21 +
    1.22  lemma eq_mem_trans: "a=b ==> b \<in> A ==> a \<in> A"
    1.23    by simp
    1.24  
    1.25 @@ -1829,6 +1837,10 @@
    1.26    "x \<in> Set.project P A \<longleftrightarrow> x \<in> A \<and> P x"
    1.27    by (simp add: project_def)
    1.28  
    1.29 +lemma inter_project [code]:
    1.30 +  "A \<inter> B = Set.project (\<lambda>x. x \<in> A) B"
    1.31 +  by (auto simp add: project_def)
    1.32 +
    1.33  instantiation set :: (equal) equal
    1.34  begin
    1.35