equal
deleted
inserted
replaced
6 Sledgehammer's heart. |
6 Sledgehammer's heart. |
7 *) |
7 *) |
8 |
8 |
9 signature SLEDGEHAMMER_RUN = |
9 signature SLEDGEHAMMER_RUN = |
10 sig |
10 sig |
11 type minimize_command = ATP_Reconstruct.minimize_command |
11 type minimize_command = ATP_Proof_Reconstruct.minimize_command |
12 type relevance_override = Sledgehammer_Filter.relevance_override |
12 type relevance_override = Sledgehammer_Filter.relevance_override |
13 type mode = Sledgehammer_Provers.mode |
13 type mode = Sledgehammer_Provers.mode |
14 type params = Sledgehammer_Provers.params |
14 type params = Sledgehammer_Provers.params |
15 type prover = Sledgehammer_Provers.prover |
15 type prover = Sledgehammer_Provers.prover |
16 |
16 |
29 |
29 |
30 structure Sledgehammer_Run : SLEDGEHAMMER_RUN = |
30 structure Sledgehammer_Run : SLEDGEHAMMER_RUN = |
31 struct |
31 struct |
32 |
32 |
33 open ATP_Util |
33 open ATP_Util |
34 open ATP_Translate |
34 open ATP_Problem_Generate |
35 open ATP_Reconstruct |
35 open ATP_Proof_Reconstruct |
36 open Sledgehammer_Util |
36 open Sledgehammer_Util |
37 open Sledgehammer_Filter |
37 open Sledgehammer_Filter |
38 open Sledgehammer_Provers |
38 open Sledgehammer_Provers |
39 open Sledgehammer_Minimize |
39 open Sledgehammer_Minimize |
40 |
40 |