1.1 --- a/src/HOL/Set.thy	Sun Jan 01 11:28:45 2012 +0100
     1.2 +++ b/src/HOL/Set.thy	Sun Jan 01 15:44:15 2012 +0100
     1.3 @@ -833,7 +833,7 @@
     1.4      thus ?R using `a\<noteq>b` by auto
     1.5    qed
     1.6  next
     1.7 -  assume ?R thus ?L by(auto split: if_splits)
     1.8 +  assume ?R thus ?L by (auto split: if_splits)
     1.9  qed
    1.10  
    1.11  subsubsection {* Singletons, using insert *}
    1.12 @@ -1796,7 +1796,7 @@
    1.13    by (auto simp add: bind_def)
    1.14  
    1.15  lemma empty_bind [simp]:
    1.16 -  "Set.bind {} B = {}"
    1.17 +  "Set.bind {} f = {}"
    1.18    by (simp add: bind_def)
    1.19  
    1.20  lemma nonempty_bind_const:
    1.21 @@ -1819,11 +1819,19 @@
    1.22  
    1.23  hide_const (open) remove
    1.24  
    1.25 +lemma member_remove [simp]:
    1.26 +  "x \<in> Set.remove y A \<longleftrightarrow> x \<in> A \<and> x \<noteq> y"
    1.27 +  by (simp add: remove_def)
    1.28 +
    1.29  definition project :: "('a \<Rightarrow> bool) \<Rightarrow> 'a set \<Rightarrow> 'a set" where
    1.30    [code_abbrev]: "project P A = {a \<in> A. P a}"
    1.31  
    1.32  hide_const (open) project
    1.33  
    1.34 +lemma member_project [simp]:
    1.35 +  "x \<in> Set.project P A \<longleftrightarrow> x \<in> A \<and> P x"
    1.36 +  by (simp add: project_def)
    1.37 +
    1.38  instantiation set :: (equal) equal
    1.39  begin
    1.40