imp_cong2 -> imp_cong
authorberghofe
Wed Feb 14 19:27:49 2001 +0100 (2001-02-14)
changeset 111205254d35e4f7c
parent 11119 2d92ab19747b
child 11121 44db3b518ca2
imp_cong2 -> imp_cong
src/Pure/drule.ML
     1.1 --- a/src/Pure/drule.ML	Wed Feb 14 13:26:46 2001 +0100
     1.2 +++ b/src/Pure/drule.ML	Wed Feb 14 19:27:49 2001 +0100
     1.3 @@ -494,7 +494,7 @@
     1.4      val AC = read_prop "PROP A ==> PROP C"
     1.5      val A = read_prop "PROP A"
     1.6    in
     1.7 -    store_standard_thm "imp_cong2" (implies_intr ABC (equal_intr
     1.8 +    store_standard_thm "imp_cong" (implies_intr ABC (equal_intr
     1.9        (implies_intr AB (implies_intr A
    1.10          (equal_elim (implies_elim (assume ABC) (assume A))
    1.11            (implies_elim (assume AB) (assume A)))))