# HG changeset patch
# User paulson
# Date 995025521 -7200
# Node ID 34a76158cbb8cfec8dfe1cb16523b7125b513c36
# Parent  5e1e952002e5b66bfe607fcf3049960de14996f1
contrapos_pn

diff -r 5e1e952002e5 -r 34a76158cbb8 src/HOL/HOL_lemmas.ML
--- 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);