Merge

--- a/src/HOL/Set.thy	Thu Apr 30 17:00:43 2015 +0100
+++ b/src/HOL/Set.thy	Fri May 01 11:36:16 2015 +0100
@@ -1623,6 +1623,9 @@
 lemma Pow_empty [simp]: "Pow {} = {{}}"
   by (auto simp add: Pow_def)
 
+lemma Pow_singleton_iff [simp]: "Pow X = {Y} \<longleftrightarrow> X = {} \<and> Y = {}"
+by blast
+
 lemma Pow_insert: "Pow (insert a A) = Pow A \<union> (insert a ` Pow A)"
   by (blast intro: image_eqI [where ?x = "u - {a}" for u])