src/HOL/Lifting.thy
changeset 47436 d8fad618a67a
parent 47376 776254f89a18
parent 47435 e1b761c216ac
child 47501 0b9294e093db
     1.1 --- a/src/HOL/Lifting.thy	Thu Apr 12 10:13:33 2012 +0200
     1.2 +++ b/src/HOL/Lifting.thy	Thu Apr 12 11:01:15 2012 +0200
     1.3 @@ -199,19 +199,19 @@
     1.4      apply safe
     1.5      apply (drule Abs1, simp)
     1.6      apply (erule Abs2)
     1.7 -    apply (rule pred_compI)
     1.8 +    apply (rule relcomppI)
     1.9      apply (rule Rep1)
    1.10      apply (rule Rep2)
    1.11 -    apply (rule pred_compI, assumption)
    1.12 +    apply (rule relcomppI, assumption)
    1.13      apply (drule Abs1, simp)
    1.14      apply (clarsimp simp add: R2)
    1.15 -    apply (rule pred_compI, assumption)
    1.16 +    apply (rule relcomppI, assumption)
    1.17      apply (drule Abs1, simp)+
    1.18      apply (clarsimp simp add: R2)
    1.19      apply (drule Abs1, simp)+
    1.20      apply (clarsimp simp add: R2)
    1.21 -    apply (rule pred_compI, assumption)
    1.22 -    apply (rule pred_compI [rotated])
    1.23 +    apply (rule relcomppI, assumption)
    1.24 +    apply (rule relcomppI [rotated])
    1.25      apply (erule conversepI)
    1.26      apply (drule Abs1, simp)+
    1.27      apply (simp add: R2)