removed duplicate contrapos;
authorwenzelm
Tue Dec 01 14:48:24 1998 +0100 (1998-12-01)
changeset 600447705248cf80
parent 6003 b382568901f6
child 6005 45186ec4d8b6
removed duplicate contrapos;
src/FOL/IFOL.ML
     1.1 --- a/src/FOL/IFOL.ML	Tue Dec 01 14:47:52 1998 +0100
     1.2 +++ b/src/FOL/IFOL.ML	Tue Dec 01 14:48:24 1998 +0100
     1.3 @@ -61,12 +61,6 @@
     1.4  qed_goal "rev_mp" IFOL.thy "[| P;  P --> Q |] ==> Q"
     1.5   (fn prems=> [ (REPEAT (resolve_tac (prems@[mp]) 1)) ]);
     1.6  
     1.7 -qed_goal "contrapos" IFOL.thy "[| ~Q;  P==>Q |] ==> ~P"
     1.8 - (fn [major,minor]=> 
     1.9 -  [ (rtac (major RS notE RS notI) 1), 
    1.10 -    (etac minor 1) ]);
    1.11 -
    1.12 -
    1.13  (*Contrapositive of an inference rule*)
    1.14  qed_goal "contrapos" IFOL.thy "[| ~Q;  P==>Q |] ==> ~P"
    1.15   (fn [major,minor]=>