Merge
authorpaulson <lp15@cam.ac.uk>
Fri May 01 11:36:16 2015 +0100 (2015-05-01)
changeset 6016529c826137153
parent 60164 670cddd97563
parent 60161 59ebc3f2f896
child 60166 ff6c4ff5e7ab
child 60167 9a97407488cd
Merge
     1.1 --- a/src/HOL/Set.thy	Thu Apr 30 17:00:43 2015 +0100
     1.2 +++ b/src/HOL/Set.thy	Fri May 01 11:36:16 2015 +0100
     1.3 @@ -1623,6 +1623,9 @@
     1.4  lemma Pow_empty [simp]: "Pow {} = {{}}"
     1.5    by (auto simp add: Pow_def)
     1.6  
     1.7 +lemma Pow_singleton_iff [simp]: "Pow X = {Y} \<longleftrightarrow> X = {} \<and> Y = {}"
     1.8 +by blast
     1.9 +
    1.10  lemma Pow_insert: "Pow (insert a A) = Pow A \<union> (insert a ` Pow A)"
    1.11    by (blast intro: image_eqI [where ?x = "u - {a}" for u])
    1.12