src/HOL/Set.thy
changeset 55143 04448228381d
parent 54998 8601434fa334
child 55775 1557a391a858
     1.1 --- a/src/HOL/Set.thy	Sat Jan 25 21:52:04 2014 +0100
     1.2 +++ b/src/HOL/Set.thy	Sat Jan 25 22:06:07 2014 +0100
     1.3 @@ -1577,10 +1577,10 @@
     1.4    by (auto simp add: Pow_def)
     1.5  
     1.6  lemma Pow_insert: "Pow (insert a A) = Pow A \<union> (insert a ` Pow A)"
     1.7 -  by (blast intro: image_eqI [where ?x = "u - {a}", standard])
     1.8 +  by (blast intro: image_eqI [where ?x = "u - {a}" for u])
     1.9  
    1.10  lemma Pow_Compl: "Pow (- A) = {-B | B. A \<in> Pow B}"
    1.11 -  by (blast intro: exI [where ?x = "- u", standard])
    1.12 +  by (blast intro: exI [where ?x = "- u" for u])
    1.13  
    1.14  lemma Pow_UNIV [simp]: "Pow UNIV = UNIV"
    1.15    by blast