src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML
changeset 43013 3a95b1ae796d
parent 43011 5f8d74d3b297
child 43015 21b6baec55b1
equal deleted inserted replaced
43012:c01c3007e07b 43013:3a95b1ae796d
   310   member (op =) params_for_minimize o fst o unalias_raw_param
   310   member (op =) params_for_minimize o fst o unalias_raw_param
   311 fun string_for_raw_param (key, values) =
   311 fun string_for_raw_param (key, values) =
   312   key ^ (case implode_param values of "" => "" | value => " = " ^ value)
   312   key ^ (case implode_param values of "" => "" | value => " = " ^ value)
   313 
   313 
   314 fun minimize_command override_params i prover_name fact_names =
   314 fun minimize_command override_params i prover_name fact_names =
   315   sledgehammerN ^ " " ^ minN ^ " [prover = " ^ prover_name ^
   315   sledgehammerN ^ " " ^ minN ^ " [" ^ prover_name ^
   316   (override_params |> filter is_raw_param_relevant_for_minimize
   316   (override_params |> filter is_raw_param_relevant_for_minimize
   317                    |> implode o map (prefix ", " o string_for_raw_param)) ^
   317                    |> implode o map (prefix ", " o string_for_raw_param)) ^
   318   "] (" ^ space_implode " " fact_names ^ ")" ^
   318   "] (" ^ space_implode " " fact_names ^ ")" ^
   319   (if i = 1 then "" else " " ^ string_of_int i)
   319   (if i = 1 then "" else " " ^ string_of_int i)
   320 
   320