# HG changeset patch
# User wenzelm
# Date 1341500283 -7200
# Node ID 3127f9ce52fb4f9e76507c88eb8cba449d3920fe
# Parent  1440a3103af0907de924d355bfd24021c2b41cad
removed obsolete rev_contrapos (cf. 1d195de59497);

diff -r 1440a3103af0 -r 3127f9ce52fb src/HOL/HOL.thy
--- a/src/HOL/HOL.thy	Thu Jul 05 16:53:29 2012 +0200
+++ b/src/HOL/HOL.thy	Thu Jul 05 16:58:03 2012 +0200
@@ -404,14 +404,6 @@
 lemma eq_neq_eq_imp_neq: "[| x = a ; a ~= b; b = y |] ==> x ~= y"
   by (erule subst, erule ssubst, assumption)
 
-(*still used in HOLCF*)
-lemma rev_contrapos:
-  assumes pq: "P ==> Q"
-      and nq: "~Q"
-  shows "~P"
-apply (rule nq [THEN contrapos_nn])
-apply (erule pq)
-done
 
 subsubsection {*Existential quantifier*}