Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
fixed layout of Sledgehammer output
authorblanchet
Thu, 01 Apr 2010 10:26:45 +0200
changeset 36065 3fc077c4780a
parent 36064 48aec67c284f
child 36066 1493b43204e9
fixed layout of Sledgehammer output
src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML file | annotate | diff | comparison | revisions 
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML	Mon Mar 29 19:49:57 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML	Thu Apr 01 10:26:45 2010 +0200
@@ -548,10 +548,10 @@
   Markup.markup Markup.sendback (metis_command i n xs) ^ ".\n" 
 fun minimize_line _ [] = ""
   | minimize_line name xs =
-      "To minimize the number of lemmas, try this command:\n" ^
+      "To minimize the number of lemmas, try this command: " ^
       Markup.markup Markup.sendback
                     ("sledgehammer minimize [atps = " ^ name ^ "] (" ^
-                     space_implode " " xs ^ ")") ^ "."
+                     space_implode " " xs ^ ")") ^ ".\n"
 
 fun metis_lemma_list dfg name (result as (_, _, _, _, goal, i)) =
   let
isabelle