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