author | oheimb |
Fri, 07 Nov 1997 17:51:26 +0100 | |
changeset 4187 | 2fafec5868fe |
parent 4186 | e39f28f94cf8 |
child 4188 | 1025a27b08f9 |
src/FOL/IFOL.ML | file | annotate | diff | comparison | revisions |
--- a/src/FOL/IFOL.ML Fri Nov 07 17:51:10 1997 +0100 +++ b/src/FOL/IFOL.ML Fri Nov 07 17:51:26 1997 +0100 @@ -61,6 +61,11 @@ 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"