new simp rule

--- a/src/HOL/Set.thy	Thu Apr 30 16:07:43 2015 +0200
+++ b/src/HOL/Set.thy	Fri May 01 08:45:30 2015 +0200
@@ -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])