src/HOL/BNF_Cardinal_Order_Relation.thy
changeset 56077 d397030fb27e
parent 56075 c6d4425f1fdc
child 56191 159b0c88b4a4
     1.1 --- a/src/HOL/BNF_Cardinal_Order_Relation.thy	Thu Mar 13 08:56:08 2014 +0100
     1.2 +++ b/src/HOL/BNF_Cardinal_Order_Relation.thy	Thu Mar 13 08:56:08 2014 +0100
     1.3 @@ -600,7 +600,7 @@
     1.4  shows "|B| \<le>o |B \<times> A|"
     1.5  proof(cases "B = {}", simp add: card_of_empty)
     1.6    assume *: "B \<noteq> {}"
     1.7 -  have "fst `(B \<times> A) = B" unfolding image_def using assms by auto
     1.8 +  have "fst `(B \<times> A) = B" using assms by auto
     1.9    thus ?thesis using inj_on_iff_surj[of B "B \<times> A"]
    1.10                       card_of_ordLeq[of B "B \<times> A"] * by blast
    1.11  qed
    1.12 @@ -1652,7 +1652,7 @@
    1.13      hence "\<forall> a. \<exists> b. h a = b" unfolding Func_def by auto
    1.14      then obtain f where f: "\<forall> a. h a = f a" by blast
    1.15      hence "range f \<subseteq> B" using h unfolding Func_def by auto
    1.16 -    thus "h \<in> (\<lambda>f a. f a) ` {f. range f \<subseteq> B}" using f unfolding image_def by auto
    1.17 +    thus "h \<in> (\<lambda>f a. f a) ` {f. range f \<subseteq> B}" using f by auto
    1.18    qed(unfold Func_def fun_eq_iff, auto)
    1.19  qed
    1.20