| author | berghofe | 
| Wed, 14 Feb 2001 19:27:49 +0100 | |
| changeset 11120 | 5254d35e4f7c | 
| parent 11119 | 2d92ab19747b | 
| child 11121 | 44db3b518ca2 | 
| src/Pure/drule.ML | file | annotate | diff | comparison | revisions | 
--- a/src/Pure/drule.ML Wed Feb 14 13:26:46 2001 +0100 +++ b/src/Pure/drule.ML Wed Feb 14 19:27:49 2001 +0100 @@ -494,7 +494,7 @@ val AC = read_prop "PROP A ==> PROP C" val A = read_prop "PROP A" in - store_standard_thm "imp_cong2" (implies_intr ABC (equal_intr + store_standard_thm "imp_cong" (implies_intr ABC (equal_intr (implies_intr AB (implies_intr A (equal_elim (implies_elim (assume ABC) (assume A)) (implies_elim (assume AB) (assume A)))))