src/HOL/HOL.thy
changeset 20223 89d2758ecddf
parent 20172 b65eb8145f5e
child 20380 14f9f2a1caa6
     1.1 --- a/src/HOL/HOL.thy	Thu Jul 27 13:42:59 2006 +0200
     1.2 +++ b/src/HOL/HOL.thy	Thu Jul 27 13:43:00 2006 +0200
     1.3 @@ -914,14 +914,15 @@
     1.4  
     1.5  use "cladata.ML"
     1.6  setup hypsubst_setup
     1.7 -
     1.8  setup {* ContextRules.addSWrapper (fn tac => hyp_subst_tac' ORELSE' tac) *}
     1.9 -
    1.10  setup Classical.setup
    1.11 +setup ResAtpSet.setup
    1.12 +setup clasetup
    1.13  
    1.14 -setup ResAtpSet.setup
    1.15 -
    1.16 -setup clasetup
    1.17 +lemma contrapos_np: "~ Q ==> (~ P ==> Q) ==> P"
    1.18 +  apply (erule swap)
    1.19 +  apply (erule (1) meta_mp)
    1.20 +  done
    1.21  
    1.22  declare ex_ex1I [rule del, intro! 2]
    1.23    and ex1I [intro]