removed obsolete rev_contrapos (cf. 1d195de59497);
authorwenzelm
Thu Jul 05 16:58:03 2012 +0200 (2012-07-05)
changeset 481953127f9ce52fb
parent 48194 1440a3103af0
child 48196 b7313810b6e6
removed obsolete rev_contrapos (cf. 1d195de59497);
src/HOL/HOL.thy
     1.1 --- a/src/HOL/HOL.thy	Thu Jul 05 16:53:29 2012 +0200
     1.2 +++ b/src/HOL/HOL.thy	Thu Jul 05 16:58:03 2012 +0200
     1.3 @@ -404,14 +404,6 @@
     1.4  lemma eq_neq_eq_imp_neq: "[| x = a ; a ~= b; b = y |] ==> x ~= y"
     1.5    by (erule subst, erule ssubst, assumption)
     1.6  
     1.7 -(*still used in HOLCF*)
     1.8 -lemma rev_contrapos:
     1.9 -  assumes pq: "P ==> Q"
    1.10 -      and nq: "~Q"
    1.11 -  shows "~P"
    1.12 -apply (rule nq [THEN contrapos_nn])
    1.13 -apply (erule pq)
    1.14 -done
    1.15  
    1.16  subsubsection {*Existential quantifier*}
    1.17