# HG changeset patch
# User nipkow
# Date 1430462730 -7200
# Node ID 59ebc3f2f8960033ebecc8e7fecc9d1ad56e42cc
# Parent  52aa014308cb1d3176d3b4961677976d65657282
new simp rule

diff -r 52aa014308cb -r 59ebc3f2f896 src/HOL/Set.thy
--- 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])