equal
deleted
inserted
replaced
15 atps: string list, |
15 atps: string list, |
16 full_types: bool, |
16 full_types: bool, |
17 respect_no_atp: bool, |
17 respect_no_atp: bool, |
18 relevance_threshold: real, |
18 relevance_threshold: real, |
19 convergence: real, |
19 convergence: real, |
|
20 theory_const: bool option, |
20 higher_order: bool option, |
21 higher_order: bool option, |
21 follow_defs: bool, |
22 follow_defs: bool, |
22 isar_proof: bool, |
23 isar_proof: bool, |
23 timeout: Time.time, |
24 timeout: Time.time, |
24 minimize_timeout: Time.time} |
25 minimize_timeout: Time.time} |
55 |
56 |
56 type relevance_override = Sledgehammer_Fact_Filter.relevance_override |
57 type relevance_override = Sledgehammer_Fact_Filter.relevance_override |
57 |
58 |
58 (** parameters, problems, results, and provers **) |
59 (** parameters, problems, results, and provers **) |
59 |
60 |
60 (* TODO: "theory_const" *) |
|
61 type params = |
61 type params = |
62 {debug: bool, |
62 {debug: bool, |
63 verbose: bool, |
63 verbose: bool, |
64 atps: string list, |
64 atps: string list, |
65 full_types: bool, |
65 full_types: bool, |
66 respect_no_atp: bool, |
66 respect_no_atp: bool, |
67 relevance_threshold: real, |
67 relevance_threshold: real, |
68 convergence: real, |
68 convergence: real, |
|
69 theory_const: bool option, |
69 higher_order: bool option, |
70 higher_order: bool option, |
70 follow_defs: bool, |
71 follow_defs: bool, |
71 isar_proof: bool, |
72 isar_proof: bool, |
72 timeout: Time.time, |
73 timeout: Time.time, |
73 minimize_timeout: Time.time} |
74 minimize_timeout: Time.time} |