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]=>