src/HOL/Wellfounded.thy

   apply (erule_tac x="{a. a \<in> A \<and> (\<exists>b\<in>A. (b, a) \<in> r i) }" in allE)
   apply (blast elim!: allE)
   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>
+  "\<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)"
   by (rule wf_UN[to_pred]) simp_all
 
 lemma wf_Union:
   assumes "\<forall>r\<in>R. wf r"