src/HOL/Quotient_Examples/FSet.thy

     show "(list_all2 R OOO op \<approx>) r r" by (rule compose_list_refl[OF e])
     show "(list_all2 R OOO op \<approx>) s s" by (rule compose_list_refl[OF e])
   next
     assume a: "(list_all2 R OOO op \<approx>) r s"
     then have b: "map Abs r \<approx> map Abs s"
-    proof (elim pred_compE)
+    proof (elim relcomppE)
       fix b ba
       assume c: "list_all2 R r b"
       assume d: "b \<approx> ba"
       assume e: "list_all2 R ba s"
       have f: "map Abs r = map Abs b"

     have b: "map Rep (map Abs r) \<approx> map Rep (map Abs s)"
       by (rule map_list_eq_cong[OF d])
     have y: "list_all2 R (map Rep (map Abs s)) s"
       by (fact rep_abs_rsp_left[OF list_quotient3[OF q], OF list_all2_refl'[OF e, of s]])
     have c: "(op \<approx> OO list_all2 R) (map Rep (map Abs r)) s"
-      by (rule pred_compI) (rule b, rule y)
+      by (rule relcomppI) (rule b, rule y)
     have z: "list_all2 R r (map Rep (map Abs r))"
       by (fact rep_abs_rsp[OF list_quotient3[OF q], OF list_all2_refl'[OF e, of r]])
     then show "(list_all2 R OOO op \<approx>) r s"
-      using a c pred_compI by simp
+      using a c relcomppI by simp
   qed
 qed
 
 lemma quotient_compose_list[quot_thm]:
   shows  "Quotient3 ((list_all2 op \<approx>) OOO (op \<approx>))

 qed
 
 quotient_definition
   "concat_fset :: ('a fset) fset \<Rightarrow> 'a fset"
   is concat 
-proof (elim pred_compE)
+proof (elim relcomppE)
 fix a b ba bb
   assume a: "list_all2 op \<approx> a ba"
   with list_symp [OF list_eq_symp] have a': "list_all2 op \<approx> ba a" by (rule sympE)
   assume b: "ba \<approx> bb"
   with list_eq_symp have b': "bb \<approx> ba" by (rule sympE)

   by (rule compose_list_refl, rule list_eq_equivp)
 
 lemma Cons_rsp2 [quot_respect]:
   shows "(op \<approx> ===> list_all2 op \<approx> OOO op \<approx> ===> list_all2 op \<approx> OOO op \<approx>) Cons Cons"
   apply (auto intro!: fun_relI)
-  apply (rule_tac b="x # b" in pred_compI)
+  apply (rule_tac b="x # b" in relcomppI)
   apply auto
-  apply (rule_tac b="x # ba" in pred_compI)
+  apply (rule_tac b="x # ba" in relcomppI)
   apply auto
   done
 
 lemma Nil_prs2 [quot_preserve]:
   assumes "Quotient3 R Abs Rep"

 
 lemma compositional_rsp3:
   assumes "(R1 ===> R2 ===> R3) C C" and "(R4 ===> R5 ===> R6) C C"
   shows "(R1 OOO R4 ===> R2 OOO R5 ===> R3 OOO R6) C C"
   by (auto intro!: fun_relI)
-     (metis (full_types) assms fun_relE pred_compI)
+     (metis (full_types) assms fun_relE relcomppI)
 
 lemma append_rsp2 [quot_respect]:
   "(list_all2 op \<approx> OOO op \<approx> ===> list_all2 op \<approx> OOO op \<approx> ===> list_all2 op \<approx> OOO op \<approx>) append append"
   by (intro compositional_rsp3)
      (auto intro!: fun_relI simp add: append_rsp2_pre)

   have c: "(list_all2 op \<approx>) (map f y) (map f' ya)"
     using y fs
     by (induct y ya rule: list_induct2')
        (simp_all, metis apply_rsp' list_eq_def)
   show "(list_all2 op \<approx> OOO op \<approx>) (map f xa) (map f' ya)"
-    by (metis a b c list_eq_def pred_compI)
+    by (metis a b c list_eq_def relcomppI)
 qed
 
 lemma map_prs2 [quot_preserve]:
   shows "((abs_fset ---> rep_fset) ---> (map rep_fset \<circ> rep_fset) ---> abs_fset \<circ> map abs_fset) map = (id ---> rep_fset ---> abs_fset) map"
   by (auto simp add: fun_eq_iff)