equal
deleted
inserted
replaced
22 |
22 |
23 open Sledgehammer_Filter |
23 open Sledgehammer_Filter |
24 |
24 |
25 fun run_prover override_params relevance_override i n ctxt goal = |
25 fun run_prover override_params relevance_override i n ctxt goal = |
26 let |
26 let |
|
27 val mode = Sledgehammer_Provers.Normal |
27 val chained_ths = [] (* a tactic has no chained ths *) |
28 val chained_ths = [] (* a tactic has no chained ths *) |
28 val params as {provers, relevance_thresholds, max_relevant, slice, ...} = |
29 val params as {provers, relevance_thresholds, max_relevant, slice, ...} = |
29 Sledgehammer_Isar.default_params ctxt override_params |
30 Sledgehammer_Isar.default_params ctxt override_params |
30 val name = hd provers |
31 val name = hd provers |
31 val prover = |
32 val prover = Sledgehammer_Provers.get_prover ctxt mode name |
32 Sledgehammer_Provers.get_prover ctxt Sledgehammer_Provers.Normal name |
|
33 val default_max_relevant = |
33 val default_max_relevant = |
34 Sledgehammer_Provers.default_max_relevant_for_prover ctxt slice name |
34 Sledgehammer_Provers.default_max_relevant_for_prover ctxt slice name |
35 val is_built_in_const = |
35 val is_built_in_const = |
36 Sledgehammer_Provers.is_built_in_const_for_prover ctxt name |
36 Sledgehammer_Provers.is_built_in_const_for_prover ctxt name |
37 val relevance_fudge = |
37 val relevance_fudge = |