src/HOL/Wellfounded.thy
changeset 56218 1c3f1f2431f9
parent 56166 9a241bc276cd
child 56375 32e0da92c786
     1.1 --- a/src/HOL/Wellfounded.thy	Wed Mar 19 17:06:02 2014 +0000
     1.2 +++ b/src/HOL/Wellfounded.thy	Wed Mar 19 18:47:22 2014 +0100
     1.3 @@ -297,7 +297,7 @@
     1.4  done
     1.5  
     1.6  lemma wfP_SUP:
     1.7 -  "\<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.8 +  "\<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 (SUPREMUM UNIV r)"
     1.9    apply (rule wf_UN[to_pred])
    1.10    apply simp_all
    1.11    done