equal
deleted
inserted
replaced
7 *) |
7 *) |
8 |
8 |
9 signature ATP_MANAGER = |
9 signature ATP_MANAGER = |
10 sig |
10 sig |
11 type cnf_thm = Clausifier.cnf_thm |
11 type cnf_thm = Clausifier.cnf_thm |
12 type name_pool = Sledgehammer_FOL_Clause.name_pool |
12 type name_pool = Metis_Clauses.name_pool |
13 type relevance_override = Sledgehammer_Fact_Filter.relevance_override |
13 type relevance_override = Sledgehammer_Fact_Filter.relevance_override |
14 type minimize_command = Sledgehammer_Proof_Reconstruct.minimize_command |
14 type minimize_command = Sledgehammer_Proof_Reconstruct.minimize_command |
15 type params = |
15 type params = |
16 {debug: bool, |
16 {debug: bool, |
17 verbose: bool, |
17 verbose: bool, |
63 end; |
63 end; |
64 |
64 |
65 structure ATP_Manager : ATP_MANAGER = |
65 structure ATP_Manager : ATP_MANAGER = |
66 struct |
66 struct |
67 |
67 |
68 open Sledgehammer_Util |
68 open Metis_Clauses |
69 open Sledgehammer_Fact_Filter |
69 open Sledgehammer_Fact_Filter |
70 open Sledgehammer_FOL_Clause |
|
71 open Sledgehammer_Proof_Reconstruct |
70 open Sledgehammer_Proof_Reconstruct |
72 |
71 |
73 (** problems, results, provers, etc. **) |
72 (** problems, results, provers, etc. **) |
74 |
73 |
75 type params = |
74 type params = |