contrapos_pn

--- a/src/HOL/HOL_lemmas.ML	Fri Jul 13 11:31:05 2001 +0200
+++ b/src/HOL/HOL_lemmas.ML	Fri Jul 13 13:58:41 2001 +0200
@@ -201,6 +201,13 @@
 by (etac minor 1) ;
 qed "contrapos_nn";
 
+(*not used at all, but we already have the other 3 combinations *)
+val [major,minor] = Goal "[| Q;  P ==> ~Q |] ==> ~P";
+by (rtac (minor RS notE RS notI) 1);
+by (assume_tac 1);
+by (rtac major 1) ;
+qed "contrapos_pn";
+
 Goal "t ~= s ==> s ~= t";
 by (etac contrapos_nn 1); 
 by (etac sym 1);