# HG changeset patch
# User oheimb
# Date 878921470 -3600
# Node ID e39f28f94cf8df5963109d333cab420acf911f0c
# Parent  71a79ac5516f3d90e15edcab0dee7a934b614910
added contrapos2

diff -r 71a79ac5516f -r e39f28f94cf8 src/FOL/FOL.ML
--- 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 ***)