changeset 17905 | 1574533861b1 |
child 17907 | c20e4bddcb11 |
17904:21c6894b5998 | 17905:1574533861b1 |
---|---|
1 (* ID: $Id$ |
|
2 Author: Jia Meng |
|
3 |
|
4 setup vampire prover as an oracle |
|
5 setup E prover as an oracle |
|
6 *) |
|
7 |
|
8 theory ResAtpOracle |
|
9 imports HOL |
|
10 uses "Tools/res_atp_setup.ML" |
|
11 "Tools/res_atp_provers.ML" |
|
12 |
|
13 begin |
|
14 |
|
15 |
|
16 |
|
17 |
|
18 oracle vampire_oracle ("string list * int") = {*ResAtpProvers.vampire_o |
|
19 *} |
|
20 |
|
21 |
|
22 |
|
23 |
|
24 oracle eprover_oracle ("string list * int") = {*ResAtpProvers.eprover_o |
|
25 *} |
|
26 |
|
27 |
|
28 end |