equal
deleted
inserted
replaced
59 (if verbose then |
59 (if verbose then |
60 " with " ^ string_of_int num_facts ^ " fact" ^ plural_s num_facts |
60 " with " ^ string_of_int num_facts ^ " fact" ^ plural_s num_facts |
61 else |
61 else |
62 "") ^ |
62 "") ^ |
63 " on " ^ (if n = 1 then "goal" else "subgoal " ^ string_of_int i) ^ |
63 " on " ^ (if n = 1 then "goal" else "subgoal " ^ string_of_int i) ^ |
64 (if blocking then |
64 (if blocking then "." |
65 "." |
65 else "\n" ^ Syntax.string_of_term ctxt (Thm.term_of (Thm.cprem_of goal i)))) |
66 else |
|
67 "\n" ^ Syntax.string_of_term ctxt (Thm.term_of (Thm.cprem_of goal i)))) |
|
68 |
66 |
69 val auto_minimize_min_facts = |
67 val auto_minimize_min_facts = |
70 Attrib.setup_config_int @{binding sledgehammer_auto_minimize_min_facts} |
68 Attrib.setup_config_int @{binding sledgehammer_auto_minimize_min_facts} |
71 (fn generic => Config.get_generic generic binary_min_facts) |
69 (fn generic => Config.get_generic generic binary_min_facts) |
72 val auto_minimize_max_time = |
70 val auto_minimize_max_time = |
99 else |
97 else |
100 let val preplay = preplay () in |
98 let val preplay = preplay () in |
101 (case preplay of |
99 (case preplay of |
102 Played (reconstructor, timeout) => |
100 Played (reconstructor, timeout) => |
103 if can_min_fast_enough timeout then |
101 if can_min_fast_enough timeout then |
104 (true, prover_name_for_reconstructor reconstructor |
102 (true, prover_name_for_reconstructor reconstructor) |
105 |> the_default name) |
|
106 else |
103 else |
107 (prover_fast_enough, name) |
104 (prover_fast_enough, name) |
108 | _ => (prover_fast_enough, name), |
105 | _ => (prover_fast_enough, name), |
109 K preplay) |
106 K preplay) |
110 end |
107 end |