src/HOL/HOL.ML

--- a/src/HOL/HOL.ML	Thu Nov 16 12:18:38 1995 +0100
+++ b/src/HOL/HOL.ML	Thu Nov 16 19:50:40 1995 +0100
@@ -126,8 +126,12 @@
   [ (rtac (major RS notE RS notI) 1), 
     (etac minor 1) ]);
 
+qed_goal "rev_contrapos" HOL.thy "[| P==>Q; ~Q |] ==> ~P"
+ (fn [major,minor]=> 
+  [ (rtac (minor RS contrapos) 1), (etac major 1) ]);
+
 (* ~(?t = ?s) ==> ~(?s = ?t) *)
-val [not_sym] = compose(sym,2,contrapos);
+bind_thm("not_sym", sym COMP rev_contrapos);
 
 
 (** Existential quantifier **)