equal
deleted
inserted
replaced
14 type translated_formula = Sledgehammer_ATP_Translate.translated_formula |
14 type translated_formula = Sledgehammer_ATP_Translate.translated_formula |
15 type type_system = Sledgehammer_ATP_Translate.type_system |
15 type type_system = Sledgehammer_ATP_Translate.type_system |
16 type minimize_command = Sledgehammer_ATP_Reconstruct.minimize_command |
16 type minimize_command = Sledgehammer_ATP_Reconstruct.minimize_command |
17 |
17 |
18 type params = |
18 type params = |
19 {blocking: bool, |
19 {debug: bool, |
20 debug: bool, |
|
21 verbose: bool, |
20 verbose: bool, |
22 overlord: bool, |
21 overlord: bool, |
|
22 blocking: bool, |
23 provers: string list, |
23 provers: string list, |
24 type_sys: type_system, |
24 type_sys: type_system, |
25 explicit_apply: bool, |
25 explicit_apply: bool, |
26 relevance_thresholds: real * real, |
26 relevance_thresholds: real * real, |
27 max_relevant: int option, |
27 max_relevant: int option, |
212 val messages = Async_Manager.thread_messages das_Tool "prover" |
212 val messages = Async_Manager.thread_messages das_Tool "prover" |
213 |
213 |
214 (** problems, results, ATPs, etc. **) |
214 (** problems, results, ATPs, etc. **) |
215 |
215 |
216 type params = |
216 type params = |
217 {blocking: bool, |
217 {debug: bool, |
218 debug: bool, |
|
219 verbose: bool, |
218 verbose: bool, |
220 overlord: bool, |
219 overlord: bool, |
|
220 blocking: bool, |
221 provers: string list, |
221 provers: string list, |
222 type_sys: type_system, |
222 type_sys: type_system, |
223 explicit_apply: bool, |
223 explicit_apply: bool, |
224 relevance_thresholds: real * real, |
224 relevance_thresholds: real * real, |
225 max_relevant: int option, |
225 max_relevant: int option, |