src/HOL/Cardinals/Constructions_on_Wellorders_Base.thy
changeset 51764 67f05cb13e08
parent 49310 6e30078de4f0
     1.1 --- a/src/HOL/Cardinals/Constructions_on_Wellorders_Base.thy	Wed Apr 24 16:21:23 2013 +0200
     1.2 +++ b/src/HOL/Cardinals/Constructions_on_Wellorders_Base.thy	Wed Apr 24 16:43:19 2013 +0200
     1.3 @@ -879,7 +879,7 @@
     1.4    {assume "r' \<le>o r"
     1.5     then obtain h where "inj_on h (Field r') \<and> h ` (Field r') \<le> Field r"
     1.6     unfolding ordLeq_def using assms embed_inj_on embed_Field by blast
     1.7 -   hence False using finite_imageD finite_subset FIN INF by blast
     1.8 +   hence False using finite_imageD finite_subset FIN INF by metis
     1.9    }
    1.10    thus ?thesis using WELL WELL' ordLess_or_ordLeq by blast
    1.11  qed
    1.12 @@ -1092,7 +1092,7 @@
    1.13    have "A \<noteq> {} \<and> A \<le> Field r"
    1.14    using A_def dir_image_Field[of r f] SUB NE by blast
    1.15    then obtain a where 1: "a \<in> A \<and> (\<forall>b \<in> A. (b,a) \<notin> r)"
    1.16 -  using WF unfolding wf_eq_minimal2 by blast
    1.17 +  using WF unfolding wf_eq_minimal2 by metis
    1.18    have "\<forall>b' \<in> A'. (b',f a) \<notin> dir_image r f"
    1.19    proof(clarify)
    1.20      fix b' assume *: "b' \<in> A'" and **: "(b',f a) \<in> dir_image r f"
    1.21 @@ -1290,7 +1290,7 @@
    1.22       }
    1.23       moreover
    1.24       {assume Case42: "(wo_rel.max2 r b1 b2, wo_rel.max2 r c1 c2) \<in> r - Id"
    1.25 -      hence ?thesis using Case4 0 unfolding bsqr_def by auto
    1.26 +      hence ?thesis using Case4 0 unfolding bsqr_def by force
    1.27       }
    1.28       moreover
    1.29       {assume Case43: "wo_rel.max2 r b1 b2 = wo_rel.max2 r c1 c2 \<and> (b1,c1) \<in> r - Id"