src/HOL/Wellfounded.thy
changeset 45970 b6d0cff57d96
parent 45139 bdcaa3f3a2f4
child 46177 adac34829e10
     1.1 --- a/src/HOL/Wellfounded.thy	Sat Dec 24 15:53:10 2011 +0100
     1.2 +++ b/src/HOL/Wellfounded.thy	Sat Dec 24 15:53:10 2011 +0100
     1.3 @@ -298,8 +298,10 @@
     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 -  by (rule wf_UN [where I=UNIV and r="\<lambda>i. {(x, y). r i x y}", to_pred SUP_UN_eq2])
     1.8 -    (simp_all add: Collect_def)
     1.9 +  apply (rule wf_UN [where I=UNIV and r="\<lambda>i. {(x, y). r i x y}", to_pred SUP_UN_eq2])
    1.10 +  apply (simp_all add: inf_set_def)
    1.11 +  apply auto
    1.12 +  done
    1.13  
    1.14  lemma wf_Union: 
    1.15   "[| ALL r:R. wf r;