src/HOL/Wellfounded.thy
changeset 46177 adac34829e10
parent 45970 b6d0cff57d96
child 46333 46c2c96f5d92
     1.1 --- a/src/HOL/Wellfounded.thy	Tue Jan 10 18:12:03 2012 +0100
     1.2 +++ b/src/HOL/Wellfounded.thy	Tue Jan 10 18:12:55 2012 +0100
     1.3 @@ -298,7 +298,7 @@
     1.4  
     1.5  lemma wfP_SUP:
     1.6    "\<forall>i. wfP (r i) \<Longrightarrow> \<forall>i j. r i \<noteq> r j \<longrightarrow> inf (DomainP (r i)) (RangeP (r j)) = bot \<Longrightarrow> wfP (SUPR UNIV r)"
     1.7 -  apply (rule wf_UN [where I=UNIV and r="\<lambda>i. {(x, y). r i x y}", to_pred SUP_UN_eq2])
     1.8 +  apply (rule wf_UN [where I=UNIV and r="\<lambda>i. {(x, y). r i x y}", to_pred])
     1.9    apply (simp_all add: inf_set_def)
    1.10    apply auto
    1.11    done
    1.12 @@ -611,9 +611,9 @@
    1.13  
    1.14  lemmas wf_acc_iff = wfP_accp_iff [to_set]
    1.15  
    1.16 -lemmas acc_subset = accp_subset [to_set pred_subset_eq]
    1.17 +lemmas acc_subset = accp_subset [to_set]
    1.18  
    1.19 -lemmas acc_subset_induct = accp_subset_induct [to_set pred_subset_eq]
    1.20 +lemmas acc_subset_induct = accp_subset_induct [to_set]
    1.21  
    1.22  
    1.23  subsection {* Tools for building wellfounded relations *}