src/HOL/Cardinals/Wellfounded_More_FP.thy
 changeset 55017 2df6ad1dbd66 parent 54481 5c9819d7713b child 55023 38db7814481d
```     1.1 --- a/src/HOL/Cardinals/Wellfounded_More_FP.thy	Thu Jan 16 15:47:33 2014 +0100
1.2 +++ b/src/HOL/Cardinals/Wellfounded_More_FP.thy	Thu Jan 16 16:20:17 2014 +0100
1.3 @@ -8,7 +8,7 @@
1.4  header {* More on Well-Founded Relations (FP) *}
1.5
1.6  theory Wellfounded_More_FP
1.7 -imports Order_Relation_More_FP "~~/src/HOL/Library/Wfrec"
1.8 +imports Wfrec Order_Relation_More_FP
1.9  begin
1.10
1.11
1.12 @@ -98,7 +98,7 @@
1.13    let ?phi = "\<lambda> A. A \<noteq> {} \<longrightarrow> (\<exists>a \<in> A. \<forall>a' \<in> A. \<not> (a',a) \<in> r)"
1.14    have "wf r = (\<forall>A. ?phi A)"
1.15    by (auto simp: ex_in_conv [THEN sym], erule wfE_min, assumption, blast)
1.16 -     (rule wfI_min, metis)
1.17 +     (rule wfI_min, fast)
1.18    (*  *)
1.19    also have "(\<forall>A. ?phi A) = (\<forall>B \<le> Field r. ?phi B)"
1.20    proof
1.21 @@ -151,7 +151,7 @@
1.22    moreover
1.23    {fix A assume *: "A \<le> Field r" and **: "A \<noteq> {}"
1.24     obtain a where 1: "r = {} \<or> r = {(a,a)}" using LI
1.25 -   unfolding order_on_defs using Case1 rel.Total_subset_Id by metis
1.26 +   unfolding order_on_defs using Case1 rel.Total_subset_Id by auto
1.27     hence "A = {a} \<and> r = {(a,a)}" using * ** unfolding Field_def by blast
1.28     hence "\<exists>a \<in> A. \<forall>a' \<in> A. (a,a') \<in> r" using 1 by blast
1.29    }
```