# HG changeset patch
# User wenzelm
# Date 912520104 -3600
# Node ID 47705248cf80550509a6dbe39a128e4c2d61ddb9
# Parent  b382568901f61433d4a049769d90af04a92ff538
removed duplicate contrapos;

diff -r b382568901f6 -r 47705248cf80 src/FOL/IFOL.ML
--- a/src/FOL/IFOL.ML	Tue Dec 01 14:47:52 1998 +0100
+++ b/src/FOL/IFOL.ML	Tue Dec 01 14:48:24 1998 +0100
@@ -61,12 +61,6 @@
 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"
  (fn [major,minor]=>