equal
deleted
inserted
replaced
13 "Tools/res_clause.ML" |
13 "Tools/res_clause.ML" |
14 ("Tools/res_axioms.ML") |
14 ("Tools/res_axioms.ML") |
15 ("Tools/res_hol_clause.ML") |
15 ("Tools/res_hol_clause.ML") |
16 ("Tools/res_reconstruct.ML") |
16 ("Tools/res_reconstruct.ML") |
17 ("Tools/res_atp.ML") |
17 ("Tools/res_atp.ML") |
18 ("Tools/atp_manager.ML") |
18 ("Tools/ATP_Manager/atp_manager.ML") |
19 ("Tools/atp_wrapper.ML") |
19 ("Tools/ATP_Manager/atp_wrapper.ML") |
20 ("Tools/atp_minimal.ML") |
20 ("Tools/ATP_Manager/atp_minimal.ML") |
21 "~~/src/Tools/Metis/metis.ML" |
21 "~~/src/Tools/Metis/metis.ML" |
22 ("Tools/metis_tools.ML") |
22 ("Tools/metis_tools.ML") |
23 begin |
23 begin |
24 |
24 |
25 definition COMBI :: "'a => 'a" |
25 definition COMBI :: "'a => 'a" |
94 use "Tools/res_axioms.ML" setup ResAxioms.setup |
94 use "Tools/res_axioms.ML" setup ResAxioms.setup |
95 use "Tools/res_hol_clause.ML" |
95 use "Tools/res_hol_clause.ML" |
96 use "Tools/res_reconstruct.ML" setup ResReconstruct.setup |
96 use "Tools/res_reconstruct.ML" setup ResReconstruct.setup |
97 use "Tools/res_atp.ML" |
97 use "Tools/res_atp.ML" |
98 |
98 |
99 use "Tools/atp_manager.ML" |
99 use "Tools/ATP_Manager/atp_manager.ML" |
100 use "Tools/atp_wrapper.ML" |
100 use "Tools/ATP_Manager/atp_wrapper.ML" |
101 |
101 use "Tools/ATP_Manager/atp_minimal.ML" |
102 use "Tools/atp_minimal.ML" |
|
103 |
102 |
104 text {* basic provers *} |
103 text {* basic provers *} |
105 setup {* AtpManager.add_prover "spass" AtpWrapper.spass *} |
104 setup {* AtpManager.add_prover "spass" AtpWrapper.spass *} |
106 setup {* AtpManager.add_prover "vampire" AtpWrapper.vampire *} |
105 setup {* AtpManager.add_prover "vampire" AtpWrapper.vampire *} |
107 setup {* AtpManager.add_prover "e" AtpWrapper.eprover *} |
106 setup {* AtpManager.add_prover "e" AtpWrapper.eprover *} |