equal
deleted
inserted
replaced
842 |
842 |
843 structure Basic_Classical: BASIC_CLASSICAL = Classical; |
843 structure Basic_Classical: BASIC_CLASSICAL = Classical; |
844 open Basic_Classical; |
844 open Basic_Classical; |
845 *} |
845 *} |
846 |
846 |
847 setup {* |
|
848 ML_Antiquote.value @{binding claset} |
|
849 (Scan.succeed "Classical.claset_of ML_context") |
|
850 *} |
|
851 |
|
852 setup Classical.setup |
847 setup Classical.setup |
853 |
848 |
854 setup {* |
849 setup {* |
855 let |
850 let |
856 fun non_bool_eq (@{const_name HOL.eq}, Type (_, [T, _])) = T <> @{typ bool} |
851 fun non_bool_eq (@{const_name HOL.eq}, Type (_, [T, _])) = T <> @{typ bool} |
887 and exI [intro] |
882 and exI [intro] |
888 |
883 |
889 declare exE [elim!] |
884 declare exE [elim!] |
890 allE [elim] |
885 allE [elim] |
891 |
886 |
892 ML {* val HOL_cs = @{claset} *} |
887 ML {* val HOL_cs = claset_of @{context} *} |
893 |
888 |
894 lemma contrapos_np: "~ Q ==> (~ P ==> Q) ==> P" |
889 lemma contrapos_np: "~ Q ==> (~ P ==> Q) ==> P" |
895 apply (erule swap) |
890 apply (erule swap) |
896 apply (erule (1) meta_mp) |
891 apply (erule (1) meta_mp) |
897 done |
892 done |