equal
deleted
inserted
replaced
9 signature SLEDGEHAMMER_RUN = |
9 signature SLEDGEHAMMER_RUN = |
10 sig |
10 sig |
11 type fact = Sledgehammer_Fact.fact |
11 type fact = Sledgehammer_Fact.fact |
12 type fact_override = Sledgehammer_Fact.fact_override |
12 type fact_override = Sledgehammer_Fact.fact_override |
13 type minimize_command = Sledgehammer_Reconstructor.minimize_command |
13 type minimize_command = Sledgehammer_Reconstructor.minimize_command |
14 type mode = Sledgehammer_Provers.mode |
14 type mode = Sledgehammer_Prover.mode |
15 type params = Sledgehammer_Provers.params |
15 type params = Sledgehammer_Prover.params |
16 |
16 |
17 val someN : string |
17 val someN : string |
18 val noneN : string |
18 val noneN : string |
19 val timeoutN : string |
19 val timeoutN : string |
20 val unknownN : string |
20 val unknownN : string |
31 open ATP_Problem_Generate |
31 open ATP_Problem_Generate |
32 open ATP_Proof |
32 open ATP_Proof |
33 open ATP_Proof_Reconstruct |
33 open ATP_Proof_Reconstruct |
34 open Sledgehammer_Util |
34 open Sledgehammer_Util |
35 open Sledgehammer_Fact |
35 open Sledgehammer_Fact |
36 open Sledgehammer_Provers |
36 open Sledgehammer_Prover |
37 open Sledgehammer_Minimize |
37 open Sledgehammer_Minimize |
38 open Sledgehammer_MaSh |
38 open Sledgehammer_MaSh |
39 |
39 |
40 val someN = "some" |
40 val someN = "some" |
41 val noneN = "none" |
41 val noneN = "none" |