Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Quotient.thy
changeset 47436 d8fad618a67a
parent 47362 b1f099bdfbba
parent 47435 e1b761c216ac
child 47488 be6dd389639d 
--- a/src/HOL/Quotient.thy	Thu Apr 12 10:13:33 2012 +0200
+++ b/src/HOL/Quotient.thy	Thu Apr 12 11:01:15 2012 +0200
@@ -694,9 +694,9 @@
 apply (rule Quotient3I)
    apply (simp add: o_def Quotient3_abs_rep [OF R2] Quotient3_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 Quotient3_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 Quotient3_rep_reflp [OF R1])
   apply (rule Rep1)
   apply (rule Quotient3_rep_reflp [OF R2])
@@ -707,8 +707,8 @@
      apply (erule Quotient3_refl1 [OF R1])
     apply (drule Quotient3_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 Quotient3_symp [OF R1, THEN sympD])
     apply (rule Quotient3_rel[symmetric, OF R1, THEN iffD2])
     apply (rule conjI, erule Quotient3_refl1 [OF R1])
@@ -721,8 +721,8 @@
     apply (erule Quotient3_refl1 [OF R1])
    apply (drule Quotient3_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 Quotient3_symp [OF R1, THEN sympD])
    apply (rule Quotient3_rel[symmetric, OF R1, THEN iffD2])
    apply (rule conjI, erule Quotient3_refl2 [OF R1])
@@ -738,11 +738,11 @@
   apply (erule Quotient3_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 Quotient3_rel[symmetric, OF R1, THEN iffD2])
   apply (rule conjI, erule Quotient3_refl1 [OF R1])
   apply (simp add: Quotient3_abs_rep [OF R1] Quotient3_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 Quotient3_rel[symmetric, OF R1, THEN iffD2])
   apply (simp add: Quotient3_abs_rep [OF R1] Quotient3_rep_reflp [OF R1])
   apply (erule Quotient3_refl2 [OF R1])
isabelle