equal
deleted
inserted
replaced
18 ("Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML") |
18 ("Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML") |
19 ("Tools/Sledgehammer/sledgehammer_fact_filter.ML") |
19 ("Tools/Sledgehammer/sledgehammer_fact_filter.ML") |
20 ("Tools/ATP_Manager/atp_manager.ML") |
20 ("Tools/ATP_Manager/atp_manager.ML") |
21 ("Tools/ATP_Manager/atp_wrapper.ML") |
21 ("Tools/ATP_Manager/atp_wrapper.ML") |
22 ("Tools/ATP_Manager/atp_minimal.ML") |
22 ("Tools/ATP_Manager/atp_minimal.ML") |
|
23 ("Tools/Sledgehammer/sledgehammer_isar.ML") |
23 ("Tools/Sledgehammer/meson_tactic.ML") |
24 ("Tools/Sledgehammer/meson_tactic.ML") |
24 ("Tools/Sledgehammer/metis_tactics.ML") |
25 ("Tools/Sledgehammer/metis_tactics.ML") |
25 begin |
26 begin |
26 |
27 |
27 definition COMBI :: "'a \<Rightarrow> 'a" |
28 definition COMBI :: "'a \<Rightarrow> 'a" |
88 apply (rule eq_reflection) |
89 apply (rule eq_reflection) |
89 apply (rule ext) |
90 apply (rule ext) |
90 apply (simp add: COMBC_def) |
91 apply (simp add: COMBC_def) |
91 done |
92 done |
92 |
93 |
|
94 |
93 subsection {* Setup of external ATPs *} |
95 subsection {* Setup of external ATPs *} |
94 |
96 |
95 use "Tools/Sledgehammer/sledgehammer_fol_clause.ML" |
97 use "Tools/Sledgehammer/sledgehammer_fol_clause.ML" |
96 use "Tools/Sledgehammer/sledgehammer_fact_preprocessor.ML" |
98 use "Tools/Sledgehammer/sledgehammer_fact_preprocessor.ML" |
97 setup Sledgehammer_Fact_Preprocessor.setup |
99 setup Sledgehammer_Fact_Preprocessor.setup |
120 text {* remote provers via SystemOnTPTP *} |
122 text {* remote provers via SystemOnTPTP *} |
121 setup {* ATP_Manager.add_prover ATP_Wrapper.remote_vampire *} |
123 setup {* ATP_Manager.add_prover ATP_Wrapper.remote_vampire *} |
122 setup {* ATP_Manager.add_prover ATP_Wrapper.remote_spass *} |
124 setup {* ATP_Manager.add_prover ATP_Wrapper.remote_spass *} |
123 setup {* ATP_Manager.add_prover ATP_Wrapper.remote_eprover *} |
125 setup {* ATP_Manager.add_prover ATP_Wrapper.remote_eprover *} |
124 |
126 |
|
127 use "Tools/Sledgehammer/sledgehammer_isar.ML" |
|
128 |
125 |
129 |
126 subsection {* The MESON prover *} |
130 subsection {* The MESON prover *} |
127 |
131 |
128 use "Tools/Sledgehammer/meson_tactic.ML" |
132 use "Tools/Sledgehammer/meson_tactic.ML" |
129 setup Meson_Tactic.setup |
133 setup Meson_Tactic.setup |