src/FOL/FOL.ML
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 ***)