--- a/src/HOL/Cardinals/Order_Union.thy Thu Jan 16 18:26:41 2014 +0100
+++ b/src/HOL/Cardinals/Order_Union.thy Thu Jan 16 18:37:37 2014 +0100
@@ -31,7 +31,7 @@
assume Case1: "B \<noteq> {}"
hence "B \<noteq> {} \<and> B \<le> Field r" using B_def by auto
then obtain a where 1: "a \<in> B" and 2: "\<forall>a1 \<in> B. (a1,a) \<notin> r"
- using WF unfolding wf_eq_minimal2 by metis
+ using WF unfolding wf_eq_minimal2 by blast
hence 3: "a \<in> Field r \<and> a \<notin> Field r'" using B_def FLD by auto
(* *)
have "\<forall>a1 \<in> A. (a1,a) \<notin> r Osum r'"
@@ -59,7 +59,7 @@
assume Case2: "B = {}"
hence 1: "A \<noteq> {} \<and> A \<le> Field r'" using * ** B_def by auto
then obtain a' where 2: "a' \<in> A" and 3: "\<forall>a1' \<in> A. (a1',a') \<notin> r'"
- using WF' unfolding wf_eq_minimal2 by metis
+ using WF' unfolding wf_eq_minimal2 by blast
hence 4: "a' \<in> Field r' \<and> a' \<notin> Field r" using 1 FLD by blast
(* *)
have "\<forall>a1' \<in> A. (a1',a') \<notin> r Osum r'"
@@ -338,7 +338,7 @@
using 1 WF' wf_Un[of "Field r \<times> Field r'" "r' - Id"]
by (auto simp add: Un_commute)
}
- ultimately have ?thesis by (metis wf_subset)
+ ultimately have ?thesis using wf_subset by blast
}
moreover
{assume Case22: "r' \<le> Id"
@@ -351,7 +351,7 @@
using 1 WF wf_Un[of "r - Id" "Field r \<times> Field r'"]
by (auto simp add: Un_commute)
}
- ultimately have ?thesis by (metis wf_subset)
+ ultimately have ?thesis using wf_subset by blast
}
ultimately show ?thesis by blast
qed