# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1430476576 -3600
# Node ID 29c826137153659a8dc86796eb16ca090fb9c4a3
# Parent  670cddd9756327c8418566e24ada0c6100ce16dc# Parent  59ebc3f2f8960033ebecc8e7fecc9d1ad56e42cc
Merge

diff -r 670cddd97563 -r 29c826137153 src/HOL/Set.thy
--- 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])