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
```