equal
deleted
inserted
replaced
20 struct |
20 struct |
21 |
21 |
22 open ATP_Util |
22 open ATP_Util |
23 open ATP_Systems |
23 open ATP_Systems |
24 open ATP_Translate |
24 open ATP_Translate |
|
25 open ATP_Reconstruct |
25 open Sledgehammer_Util |
26 open Sledgehammer_Util |
26 open Sledgehammer_Filter |
27 open Sledgehammer_Filter |
27 open Sledgehammer_Provers |
28 open Sledgehammer_Provers |
28 open Sledgehammer_Minimize |
29 open Sledgehammer_Minimize |
29 open Sledgehammer_Run |
30 open Sledgehammer_Run |
308 fun get_params mode = extract_params mode o default_raw_params |
309 fun get_params mode = extract_params mode o default_raw_params |
309 fun default_params thy = get_params Normal thy o map (apsnd single) |
310 fun default_params thy = get_params Normal thy o map (apsnd single) |
310 |
311 |
311 (* Sledgehammer the given subgoal *) |
312 (* Sledgehammer the given subgoal *) |
312 |
313 |
313 val default_minimize_prover = Metis_Tactic.metisN |
314 val default_minimize_prover = metisN |
314 |
315 |
315 fun is_raw_param_relevant_for_minimize (name, _) = |
316 fun is_raw_param_relevant_for_minimize (name, _) = |
316 member (op =) params_for_minimize name |
317 member (op =) params_for_minimize name |
317 fun string_for_raw_param (key, values) = |
318 fun string_for_raw_param (key, values) = |
318 key ^ (case implode_param values of "" => "" | value => " = " ^ value) |
319 key ^ (case implode_param values of "" => "" | value => " = " ^ value) |