diff -r 894d6d863823 -r 86fa63ce8156 src/HOL/Set.thy
--- a/src/HOL/Set.thy	Mon Apr 13 13:03:41 2015 +0200
+++ b/src/HOL/Set.thy	Tue Apr 14 11:32:01 2015 +0200
@@ -647,7 +647,6 @@
 lemma empty_not_UNIV[simp]: "{} \<noteq> UNIV"
 by blast
 
-
 subsubsection {* The Powerset operator -- Pow *}
 
 definition Pow :: "'a set => 'a set set" where
@@ -846,6 +845,9 @@
   assume ?R thus ?L by (auto split: if_splits)
 qed
 
+lemma insert_UNIV: "insert x UNIV = UNIV"
+by auto
+
 subsubsection {* Singletons, using insert *}
 
 lemma singletonI [intro!]: "a : {a}"
@@ -1884,6 +1886,8 @@
 lemma bind_const: "Set.bind A (\<lambda>_. B) = (if A = {} then {} else B)"
   by (auto simp add: bind_def)
 
+lemma bind_singleton_conv_image: "Set.bind A (\<lambda>x. {f x}) = f ` A"
+  by(auto simp add: bind_def)
 
 subsubsection {* Operations for execution *}