equal
deleted
inserted
replaced
241 (preplay, proof_banner mode name, used_facts, |
241 (preplay, proof_banner mode name, used_facts, |
242 choose_minimize_command thy params minimize_command name preplay, subgoal, |
242 choose_minimize_command thy params minimize_command name preplay, subgoal, |
243 subgoal_count) |
243 subgoal_count) |
244 val num_chained = length (#facts (Proof.goal state)) |
244 val num_chained = length (#facts (Proof.goal state)) |
245 in |
245 in |
246 one_line_proof_text num_chained one_line_params |
246 one_line_proof_text ctxt num_chained one_line_params |
247 end, |
247 end, |
248 if verbose then "\nSMT solver real CPU time: " ^ string_of_time run_time ^ "." else "") |
248 if verbose then "\nSMT solver real CPU time: " ^ string_of_time run_time ^ "." else "") |
249 | SOME failure => |
249 | SOME failure => |
250 (Lazy.value (Metis_Method (NONE, NONE), Play_Failed), |
250 (Lazy.value (Metis_Method (NONE, NONE), Play_Failed), |
251 fn _ => string_of_atp_failure failure, "")) |
251 fn _ => string_of_atp_failure failure, "")) |