--- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML Tue Mar 23 14:43:22 2010 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML Wed Mar 24 12:30:33 2010 +0100
@@ -339,18 +339,18 @@
let
val _ = trace_proof_msg (K "\n\nisar_proof_body: start\n")
val string_of_term = PrintMode.setmp [] (Syntax.string_of_term ctxt)
- fun have_or_show "show" _ = "show \""
- | have_or_show have lname = have ^ " " ^ lname ^ ": \""
+ fun have_or_show "show" _ = " show \""
+ | have_or_show have lname = " " ^ have ^ " " ^ lname ^ ": \""
fun do_line _ (lname, t, []) =
(* No deps: it's a conjecture clause, with no proof. *)
(case permuted_clause t ctms of
- SOME u => "assume " ^ lname ^ ": \"" ^ string_of_term u ^ "\"\n"
+ SOME u => " assume " ^ lname ^ ": \"" ^ string_of_term u ^ "\"\n"
| NONE => raise TERM ("Sledgehammer_Proof_Reconstruct.isar_proof_body",
[t]))
| do_line have (lname, t, deps) =
have_or_show have lname ^
string_of_term (gen_all_vars (HOLogic.mk_Trueprop t)) ^
- "\"\n by (metis " ^ space_implode " " deps ^ ")\n"
+ "\"\n by (metis " ^ space_implode " " deps ^ ")\n"
fun do_lines [(lname, t, deps)] = [do_line "show" (lname, t, deps)]
| do_lines ((lname, t, deps) :: lines) =
do_line "have" (lname, t, deps) :: do_lines lines
@@ -535,19 +535,20 @@
val kill_chained = filter_out (curry (op =) chained_hint)
(* metis-command *)
-fun metis_line [] = "apply metis"
- | metis_line xs = "apply (metis " ^ space_implode " " xs ^ ")"
+fun metis_line [] = "by metis"
+ | metis_line xs = "by (metis " ^ space_implode " " xs ^ ")"
-(* atp_minimize [atp=<prover>] <lemmas> *)
fun minimize_line _ [] = ""
| minimize_line name lemmas =
"To minimize the number of lemmas, try this command:\n" ^
- Markup.markup Markup.sendback ("atp_minimize [atp = " ^ name ^ "] " ^
- space_implode " " (kill_chained lemmas))
+ Markup.markup Markup.sendback
+ ("sledgehammer minimize [atps = " ^ name ^ "] (" ^
+ space_implode " " (kill_chained lemmas) ^ ")") ^ "."
fun metis_lemma_list dfg name result =
let val (lemmas, used_conj) = extract_lemmas (get_step_nums dfg) result in
- (Markup.markup Markup.sendback (metis_line (kill_chained lemmas)) ^ "\n" ^
+ ("Try this command: " ^
+ Markup.markup Markup.sendback (metis_line (kill_chained lemmas)) ^ ".\n" ^
minimize_line name lemmas ^
(if used_conj then
""