315 member (op =) params_for_minimize o fst o unalias_raw_param |
315 member (op =) params_for_minimize o fst o unalias_raw_param |
316 fun string_for_raw_param (key, values) = |
316 fun string_for_raw_param (key, values) = |
317 key ^ (case implode_param values of "" => "" | value => " = " ^ value) |
317 key ^ (case implode_param values of "" => "" | value => " = " ^ value) |
318 |
318 |
319 fun minimize_command override_params i prover_name fact_names = |
319 fun minimize_command override_params i prover_name fact_names = |
320 sledgehammerN ^ " " ^ minN ^ |
320 let |
321 (if prover_name = default_minimize_prover then "" |
321 val params = |
322 else enclose "[" "]" prover_name) ^ |
322 override_params |
323 (override_params |> filter is_raw_param_relevant_for_minimize |
323 |> filter is_raw_param_relevant_for_minimize |
324 |> implode o map (prefix ", " o string_for_raw_param)) ^ |
324 |> map string_for_raw_param |
325 " (" ^ space_implode " " fact_names ^ ")" ^ |
325 |> (if prover_name = default_minimize_prover then I else cons prover_name) |
326 (if i = 1 then "" else " " ^ string_of_int i) |
326 |> space_implode ", " |
|
327 in |
|
328 sledgehammerN ^ " " ^ minN ^ |
|
329 (if params = "" then "" else enclose " [" "]" params) ^ |
|
330 " (" ^ space_implode " " fact_names ^ ")" ^ |
|
331 (if i = 1 then "" else " " ^ string_of_int i) |
|
332 end |
327 |
333 |
328 fun hammer_away override_params subcommand opt_i relevance_override state = |
334 fun hammer_away override_params subcommand opt_i relevance_override state = |
329 let |
335 let |
330 val ctxt = Proof.context_of state |
336 val ctxt = Proof.context_of state |
331 val override_params = |
337 val override_params = |