# HG changeset patch
# User oheimb
# Date 878921486 -3600
# Node ID 2fafec5868fe7f9b02f9b1c6fb40657bbfa81877
# Parent  e39f28f94cf8df5963109d333cab420acf911f0c
added contrapos

diff -r e39f28f94cf8 -r 2fafec5868fe src/FOL/IFOL.ML
--- 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"