src/HOL/HOL.thy
changeset 20766 9913d3bc3d17
parent 20741 c8fdad2dc6e6
child 20833 4fcf8ddb54f5
equal deleted inserted replaced
20765:807c5f7dcb94 20766:9913d3bc3d17
     5 
     5 
     6 header {* The basis of Higher-Order Logic *}
     6 header {* The basis of Higher-Order Logic *}
     7 
     7 
     8 theory HOL
     8 theory HOL
     9 imports CPure
     9 imports CPure
    10 uses ("cladata.ML") ("blastdata.ML") ("simpdata.ML")
    10 uses ("cladata.ML") ("blastdata.ML") ("simpdata.ML") "Tools/res_atpset.ML"
    11     "Tools/res_atpset.ML"
       
    12 
       
    13 begin
    11 begin
    14 
    12 
    15 subsection {* Primitive logic *}
    13 subsection {* Primitive logic *}
    16 
    14 
    17 subsubsection {* Core syntax *}
    15 subsubsection {* Core syntax *}
   918 
   916 
   919 use "cladata.ML"
   917 use "cladata.ML"
   920 setup hypsubst_setup
   918 setup hypsubst_setup
   921 setup {* ContextRules.addSWrapper (fn tac => hyp_subst_tac' ORELSE' tac) *}
   919 setup {* ContextRules.addSWrapper (fn tac => hyp_subst_tac' ORELSE' tac) *}
   922 setup Classical.setup
   920 setup Classical.setup
   923 setup ResAtpSet.setup
   921 setup ResAtpset.setup
   924 setup clasetup
   922 setup clasetup
   925 
   923 
   926 lemma contrapos_np: "~ Q ==> (~ P ==> Q) ==> P"
   924 lemma contrapos_np: "~ Q ==> (~ P ==> Q) ==> P"
   927   apply (erule swap)
   925   apply (erule swap)
   928   apply (erule (1) meta_mp)
   926   apply (erule (1) meta_mp)