diff -r af3b95160b59 -r 53e7cc599f58 src/HOL/Set.thy
--- a/src/HOL/Set.thy	Sun Jan 01 11:28:45 2012 +0100
+++ b/src/HOL/Set.thy	Sun Jan 01 15:44:15 2012 +0100
@@ -833,7 +833,7 @@
     thus ?R using `a\<noteq>b` by auto
   qed
 next
-  assume ?R thus ?L by(auto split: if_splits)
+  assume ?R thus ?L by (auto split: if_splits)
 qed
 
 subsubsection {* Singletons, using insert *}
@@ -1796,7 +1796,7 @@
   by (auto simp add: bind_def)
 
 lemma empty_bind [simp]:
-  "Set.bind {} B = {}"
+  "Set.bind {} f = {}"
   by (simp add: bind_def)
 
 lemma nonempty_bind_const:
@@ -1819,11 +1819,19 @@
 
 hide_const (open) remove
 
+lemma member_remove [simp]:
+  "x \<in> Set.remove y A \<longleftrightarrow> x \<in> A \<and> x \<noteq> y"
+  by (simp add: remove_def)
+
 definition project :: "('a \<Rightarrow> bool) \<Rightarrow> 'a set \<Rightarrow> 'a set" where
   [code_abbrev]: "project P A = {a \<in> A. P a}"
 
 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)
+
 instantiation set :: (equal) equal
 begin