author | wenzelm |
Tue, 01 Dec 1998 14:48:24 +0100 | |
changeset 6004 | 47705248cf80 |
parent 6003 | b382568901f6 |
child 6005 | 45186ec4d8b6 |
src/FOL/IFOL.ML | file | annotate | diff | comparison | revisions |
--- a/src/FOL/IFOL.ML Tue Dec 01 14:47:52 1998 +0100 +++ b/src/FOL/IFOL.ML Tue Dec 01 14:48:24 1998 +0100 @@ -61,12 +61,6 @@ qed_goal "rev_mp" IFOL.thy "[| P; P --> Q |] ==> Q" (fn prems=> [ (REPEAT (resolve_tac (prems@[mp]) 1)) ]); -qed_goal "contrapos" IFOL.thy "[| ~Q; P==>Q |] ==> ~P" - (fn [major,minor]=> - [ (rtac (major RS notE RS notI) 1), - (etac minor 1) ]); - - (*Contrapositive of an inference rule*) qed_goal "contrapos" IFOL.thy "[| ~Q; P==>Q |] ==> ~P" (fn [major,minor]=>