equal
deleted
inserted
replaced
1 (* ID: $Id$ |
1 (* ID: $Id$ |
2 Author: Jia Meng, NICTA |
2 Author: Jia Meng, NICTA |
3 a method to setup "vampire" method |
|
4 a method to setup "eprover" method |
|
5 *) |
3 *) |
6 |
4 |
|
5 header {* ATP setup (Vampire and E prover) *} |
|
6 |
7 theory ResAtpMethods |
7 theory ResAtpMethods |
8 imports Reconstruction |
8 imports Reconstruction |
9 |
9 uses |
10 uses ("Tools/res_atp_setup.ML") |
10 "Tools/res_atp_setup.ML" |
11 ("Tools/res_atp_provers.ML") |
11 "Tools/res_atp_provers.ML" |
12 ("Tools/res_atp_methods.ML") |
12 ("Tools/res_atp_methods.ML") |
13 |
13 |
14 begin |
14 begin |
15 |
15 |
16 ML{*use "Tools/res_atp_setup.ML"*} |
16 oracle vampire_oracle ("string list * int") = {* ResAtpProvers.vampire_o *} |
17 ML{*use "Tools/res_atp_provers.ML"*} |
17 oracle eprover_oracle ("string list * int") = {* ResAtpProvers.eprover_o *} |
18 |
18 |
19 oracle vampire_oracle ("string list * int") = {*ResAtpProvers.vampire_o*} |
19 use "Tools/res_atp_methods.ML" |
20 oracle eprover_oracle ("string list * int") = {*ResAtpProvers.eprover_o*} |
20 setup ResAtpMethods.ResAtps_setup |
21 |
21 |
22 |
|
23 ML{*use "Tools/res_atp_methods.ML"*} |
|
24 |
|
25 setup ResAtpMethods.ResAtps_setup |
|
26 end |
22 end |