src/HOL/Quotient.thy
changeset 47436 d8fad618a67a
parent 47362 b1f099bdfbba
parent 47435 e1b761c216ac
child 47488 be6dd389639d
     1.1 --- a/src/HOL/Quotient.thy	Thu Apr 12 10:13:33 2012 +0200
     1.2 +++ b/src/HOL/Quotient.thy	Thu Apr 12 11:01:15 2012 +0200
     1.3 @@ -694,9 +694,9 @@
     1.4  apply (rule Quotient3I)
     1.5     apply (simp add: o_def Quotient3_abs_rep [OF R2] Quotient3_abs_rep [OF R1])
     1.6    apply simp
     1.7 -  apply (rule_tac b="Rep1 (Rep2 a)" in pred_compI)
     1.8 +  apply (rule_tac b="Rep1 (Rep2 a)" in relcomppI)
     1.9     apply (rule Quotient3_rep_reflp [OF R1])
    1.10 -  apply (rule_tac b="Rep1 (Rep2 a)" in pred_compI [rotated])
    1.11 +  apply (rule_tac b="Rep1 (Rep2 a)" in relcomppI [rotated])
    1.12     apply (rule Quotient3_rep_reflp [OF R1])
    1.13    apply (rule Rep1)
    1.14    apply (rule Quotient3_rep_reflp [OF R2])
    1.15 @@ -707,8 +707,8 @@
    1.16       apply (erule Quotient3_refl1 [OF R1])
    1.17      apply (drule Quotient3_refl1 [OF R2], drule Rep1)
    1.18      apply (subgoal_tac "R1 r (Rep1 (Abs1 x))")
    1.19 -     apply (rule_tac b="Rep1 (Abs1 x)" in pred_compI, assumption)
    1.20 -     apply (erule pred_compI)
    1.21 +     apply (rule_tac b="Rep1 (Abs1 x)" in relcomppI, assumption)
    1.22 +     apply (erule relcomppI)
    1.23       apply (erule Quotient3_symp [OF R1, THEN sympD])
    1.24      apply (rule Quotient3_rel[symmetric, OF R1, THEN iffD2])
    1.25      apply (rule conjI, erule Quotient3_refl1 [OF R1])
    1.26 @@ -721,8 +721,8 @@
    1.27      apply (erule Quotient3_refl1 [OF R1])
    1.28     apply (drule Quotient3_refl2 [OF R2], drule Rep1)
    1.29     apply (subgoal_tac "R1 s (Rep1 (Abs1 y))")
    1.30 -    apply (rule_tac b="Rep1 (Abs1 y)" in pred_compI, assumption)
    1.31 -    apply (erule pred_compI)
    1.32 +    apply (rule_tac b="Rep1 (Abs1 y)" in relcomppI, assumption)
    1.33 +    apply (erule relcomppI)
    1.34      apply (erule Quotient3_symp [OF R1, THEN sympD])
    1.35     apply (rule Quotient3_rel[symmetric, OF R1, THEN iffD2])
    1.36     apply (rule conjI, erule Quotient3_refl2 [OF R1])
    1.37 @@ -738,11 +738,11 @@
    1.38    apply (erule Quotient3_refl1 [OF R1])
    1.39   apply (rename_tac a b c d)
    1.40   apply simp
    1.41 - apply (rule_tac b="Rep1 (Abs1 r)" in pred_compI)
    1.42 + apply (rule_tac b="Rep1 (Abs1 r)" in relcomppI)
    1.43    apply (rule Quotient3_rel[symmetric, OF R1, THEN iffD2])
    1.44    apply (rule conjI, erule Quotient3_refl1 [OF R1])
    1.45    apply (simp add: Quotient3_abs_rep [OF R1] Quotient3_rep_reflp [OF R1])
    1.46 - apply (rule_tac b="Rep1 (Abs1 s)" in pred_compI [rotated])
    1.47 + apply (rule_tac b="Rep1 (Abs1 s)" in relcomppI [rotated])
    1.48    apply (rule Quotient3_rel[symmetric, OF R1, THEN iffD2])
    1.49    apply (simp add: Quotient3_abs_rep [OF R1] Quotient3_rep_reflp [OF R1])
    1.50    apply (erule Quotient3_refl2 [OF R1])