dropped abbreviation "pred_comp"; introduced infix notation "P OO Q" for "relcompp P Q"

--- a/src/HOL/Quotient.thy	Tue Apr 03 17:26:30 2012 +0900
+++ b/src/HOL/Quotient.thy	Tue Apr 03 17:45:06 2012 +0900
@@ -717,9 +717,9 @@
 apply (rule QuotientI)
    apply (simp add: o_def Quotient_abs_rep [OF R2] Quotient_abs_rep [OF R1])
   apply simp
-  apply (rule_tac b="Rep1 (Rep2 a)" in pred_compI)
+  apply (rule_tac b="Rep1 (Rep2 a)" in relcomppI)
    apply (rule Quotient_rep_reflp [OF R1])
-  apply (rule_tac b="Rep1 (Rep2 a)" in pred_compI [rotated])
+  apply (rule_tac b="Rep1 (Rep2 a)" in relcomppI [rotated])
    apply (rule Quotient_rep_reflp [OF R1])
   apply (rule Rep1)
   apply (rule Quotient_rep_reflp [OF R2])
@@ -730,8 +730,8 @@
      apply (erule Quotient_refl1 [OF R1])
     apply (drule Quotient_refl1 [OF R2], drule Rep1)
     apply (subgoal_tac "R1 r (Rep1 (Abs1 x))")
-     apply (rule_tac b="Rep1 (Abs1 x)" in pred_compI, assumption)
-     apply (erule pred_compI)
+     apply (rule_tac b="Rep1 (Abs1 x)" in relcomppI, assumption)
+     apply (erule relcomppI)
      apply (erule Quotient_symp [OF R1, THEN sympD])
     apply (rule Quotient_rel[symmetric, OF R1, THEN iffD2])
     apply (rule conjI, erule Quotient_refl1 [OF R1])
@@ -744,8 +744,8 @@
     apply (erule Quotient_refl1 [OF R1])
    apply (drule Quotient_refl2 [OF R2], drule Rep1)
    apply (subgoal_tac "R1 s (Rep1 (Abs1 y))")
-    apply (rule_tac b="Rep1 (Abs1 y)" in pred_compI, assumption)
-    apply (erule pred_compI)
+    apply (rule_tac b="Rep1 (Abs1 y)" in relcomppI, assumption)
+    apply (erule relcomppI)
     apply (erule Quotient_symp [OF R1, THEN sympD])
    apply (rule Quotient_rel[symmetric, OF R1, THEN iffD2])
    apply (rule conjI, erule Quotient_refl2 [OF R1])
@@ -761,11 +761,11 @@
   apply (erule Quotient_refl1 [OF R1])
  apply (rename_tac a b c d)
  apply simp
- apply (rule_tac b="Rep1 (Abs1 r)" in pred_compI)
+ apply (rule_tac b="Rep1 (Abs1 r)" in relcomppI)
   apply (rule Quotient_rel[symmetric, OF R1, THEN iffD2])
   apply (rule conjI, erule Quotient_refl1 [OF R1])
   apply (simp add: Quotient_abs_rep [OF R1] Quotient_rep_reflp [OF R1])
- apply (rule_tac b="Rep1 (Abs1 s)" in pred_compI [rotated])
+ apply (rule_tac b="Rep1 (Abs1 s)" in relcomppI [rotated])
   apply (rule Quotient_rel[symmetric, OF R1, THEN iffD2])
   apply (simp add: Quotient_abs_rep [OF R1] Quotient_rep_reflp [OF R1])
   apply (erule Quotient_refl2 [OF R1])

--- a/src/HOL/Quotient_Examples/FSet.thy	Tue Apr 03 17:26:30 2012 +0900
+++ b/src/HOL/Quotient_Examples/FSet.thy	Tue Apr 03 17:45:06 2012 +0900
@@ -140,7 +140,7 @@
   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"
@@ -165,11 +165,11 @@
     have y: "list_all2 R (map Rep (map Abs s)) s"
       by (fact rep_abs_rsp_left[OF list_quotient[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_quotient[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
 
@@ -360,7 +360,7 @@
 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)
@@ -397,9 +397,9 @@
 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
 
@@ -453,7 +453,7 @@
   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"
@@ -479,7 +479,7 @@
     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]:

--- a/src/HOL/Relation.thy	Tue Apr 03 17:26:30 2012 +0900
+++ b/src/HOL/Relation.thy	Tue Apr 03 17:45:06 2012 +0900
@@ -512,10 +512,9 @@
 where
   relcompI [intro]: "(a, b) \<in> r \<Longrightarrow> (b, c) \<in> s \<Longrightarrow> (a, c) \<in> r O s"
 
-abbreviation pred_comp (infixr "OO" 75) where
-  "pred_comp \<equiv> relcompp"
+notation relcompp (infixr "OO" 75)
 
-lemmas pred_compI = relcompp.intros
+lemmas relcomppI = relcompp.intros
 
 text {*
   For historic reasons, the elimination rules are not wholly corresponding.
@@ -523,14 +522,12 @@
 *}
 
 inductive_cases relcompEpair: "(a, c) \<in> r O s"
-inductive_cases pred_compE [elim!]: "(r OO s) a c"
+inductive_cases relcomppE [elim!]: "(r OO s) a c"
 
 lemma relcompE [elim!]: "xz \<in> r O s \<Longrightarrow>
   (\<And>x y z. xz = (x, z) \<Longrightarrow> (x, y) \<in> r \<Longrightarrow> (y, z) \<in> s  \<Longrightarrow> P) \<Longrightarrow> P"
   by (cases xz) (simp, erule relcompEpair, iprover)
 
-lemmas pred_comp_relcomp_eq = relcompp_relcomp_eq
-
 lemma R_O_Id [simp]:
   "R O Id = R"
   by fast
@@ -543,7 +540,7 @@
   "{} O R = {}"
   by blast
 
-lemma pred_comp_bot1 [simp]:
+lemma relcompp_bot1 [simp]:
   "\<bottom> OO R = \<bottom>"
   by (fact relcomp_empty1 [to_pred])
 
@@ -551,7 +548,7 @@
   "R O {} = {}"
   by blast
 
-lemma pred_comp_bot2 [simp]:
+lemma relcompp_bot2 [simp]:
   "R OO \<bottom> = \<bottom>"
   by (fact relcomp_empty2 [to_pred])
 
@@ -560,7 +557,7 @@
   by blast
 
 
-lemma pred_comp_assoc:
+lemma relcompp_assoc:
   "(r OO s) OO t = r OO (s OO t)"
   by (fact O_assoc [to_pred])
 
@@ -568,7 +565,7 @@
   "trans r \<Longrightarrow> r O r \<subseteq> r"
   by (unfold trans_def) blast
 
-lemma transp_pred_comp_less_eq:
+lemma transp_relcompp_less_eq:
   "transp r \<Longrightarrow> r OO r \<le> r "
   by (fact trans_O_subset [to_pred])
 
@@ -576,7 +573,7 @@
   "r' \<subseteq> r \<Longrightarrow> s' \<subseteq> s \<Longrightarrow> r' O s' \<subseteq> r O s"
   by blast
 
-lemma pred_comp_mono:
+lemma relcompp_mono:
   "r' \<le> r \<Longrightarrow> s' \<le> s \<Longrightarrow> r' OO s' \<le> r OO s "
   by (fact relcomp_mono [to_pred])
 
@@ -588,7 +585,7 @@
   "R O (S \<union> T) = (R O S) \<union> (R O T)" 
   by auto
 
-lemma pred_comp_distrib [simp]:
+lemma relcompp_distrib [simp]:
   "R OO (S \<squnion> T) = R OO S \<squnion> R OO T"
   by (fact relcomp_distrib [to_pred])
 
@@ -596,7 +593,7 @@
   "(S \<union> T) O R = (S O R) \<union> (T O R)"
   by auto
 
-lemma pred_comp_distrib2 [simp]:
+lemma relcompp_distrib2 [simp]:
   "(S \<squnion> T) OO R = S OO R \<squnion> T OO R"
   by (fact relcomp_distrib2 [to_pred])
 
@@ -679,9 +676,9 @@
 lemma converse_relcomp: "(r O s)^-1 = s^-1 O r^-1"
   by blast
 
-lemma converse_pred_comp: "(r OO s)^--1 = s^--1 OO r^--1"
-  by (iprover intro: order_antisym conversepI pred_compI
-    elim: pred_compE dest: conversepD)
+lemma converse_relcompp: "(r OO s)^--1 = s^--1 OO r^--1"
+  by (iprover intro: order_antisym conversepI relcomppI
+    elim: relcomppE dest: conversepD)
 
 lemma converse_Int: "(r \<inter> s)^-1 = r^-1 \<inter> s^-1"
   by blast