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    }