equal
deleted
inserted
replaced
30 ("~~/src/Tools/induct_tacs.ML") |
30 ("~~/src/Tools/induct_tacs.ML") |
31 ("Tools/recfun_codegen.ML") |
31 ("Tools/recfun_codegen.ML") |
32 "Tools/async_manager.ML" |
32 "Tools/async_manager.ML" |
33 "Tools/try.ML" |
33 "Tools/try.ML" |
34 ("Tools/cnf_funcs.ML") |
34 ("Tools/cnf_funcs.ML") |
35 ("Tools/type_mapper.ML") |
35 ("Tools/type_lifting.ML") |
36 "~~/src/Tools/subtyping.ML" |
36 "~~/src/Tools/subtyping.ML" |
37 begin |
37 begin |
38 |
38 |
39 setup {* Intuitionistic.method_setup @{binding iprover} *} |
39 setup {* Intuitionistic.method_setup @{binding iprover} *} |
40 setup Subtyping.setup |
40 setup Subtyping.setup |
712 lemmas [trans] = trans |
712 lemmas [trans] = trans |
713 and [sym] = sym not_sym |
713 and [sym] = sym not_sym |
714 and [Pure.elim?] = iffD1 iffD2 impE |
714 and [Pure.elim?] = iffD1 iffD2 impE |
715 |
715 |
716 use "Tools/hologic.ML" |
716 use "Tools/hologic.ML" |
717 use "Tools/type_mapper.ML" |
717 use "Tools/type_lifting.ML" |
718 |
718 |
719 |
719 |
720 subsubsection {* Atomizing meta-level connectives *} |
720 subsubsection {* Atomizing meta-level connectives *} |
721 |
721 |
722 axiomatization where |
722 axiomatization where |