equal
deleted
inserted
replaced
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) |