changeset 4186 | e39f28f94cf8 |
parent 4096 | 8cdf672a83e8 |
child 4308 | 9abce31cc764 |
--- a/src/FOL/FOL.ML Fri Nov 07 15:24:58 1997 +0100 +++ b/src/FOL/FOL.ML Fri Nov 07 17:51:10 1997 +0100 @@ -58,6 +58,11 @@ (fn [major]=> [ (rtac classical 1), (eresolve_tac [major RS notE] 1) ]); +qed_goal "contrapos2" FOL.thy "[| Q; ~ P ==> ~ Q |] ==> P" (fn [p1,p2] => [ + rtac classical 1, + dtac p2 1, + etac notE 1, + rtac p1 1]); (*** Tactics for implication and contradiction ***)