# HG changeset patch
# User blanchet
# Date 1306485008 -7200
# Node ID e437d47f419f6917d0fed9d4d6cf25dee1d0f81d
# Parent  e1172791ad0d95400c81d42f972029962d1eb47d
more concise output

diff -r e1172791ad0d -r e437d47f419f doc-src/Sledgehammer/sledgehammer.tex
--- a/doc-src/Sledgehammer/sledgehammer.tex	Fri May 27 10:30:08 2011 +0200
+++ b/doc-src/Sledgehammer/sledgehammer.tex	Fri May 27 10:30:08 2011 +0200
@@ -249,33 +249,33 @@
 \slshape
 Sledgehammer: ``\textit{e}'' on goal: \\
 $[a] = [b] \,\Longrightarrow\, a = b$ \\
-Try this command: \textbf{by} (\textit{metis last\_ConsL}). \\
+Try this: \textbf{by} (\textit{metis last\_ConsL}). \\
 To minimize: \textbf{sledgehammer} \textit{min} [\textit{e}] (\textit{last\_ConsL}). \\[3\smallskipamount]
 %
 Sledgehammer: ``\textit{vampire}'' on goal: \\
 $[a] = [b] \,\Longrightarrow\, a = b$ \\
-Try this command: \textbf{by} (\textit{metis hd.simps}). \\
+Try this: \textbf{by} (\textit{metis hd.simps}). \\
 To minimize: \textbf{sledgehammer} \textit{min} [\textit{vampire}] (\textit{hd.simps}). \\[3\smallskipamount]
 %
 Sledgehammer: ``\textit{spass}'' on goal: \\
 $[a] = [b] \,\Longrightarrow\, a = b$ \\
-Try this command: \textbf{by} (\textit{metis list.inject}). \\
+Try this: \textbf{by} (\textit{metis list.inject}). \\
 To minimize: \textbf{sledgehammer} \textit{min} [\textit{spass}]~(\textit{list.inject}). \\[3\smallskipamount]
 %
 Sledgehammer: ``\textit{remote\_waldmeister}'' on goal: \\
 $[a] = [b] \,\Longrightarrow\, a = b$ \\
-Try this command: \textbf{by} (\textit{metis hd.simps insert\_Nil}). \\
+Try this: \textbf{by} (\textit{metis hd.simps insert\_Nil}). \\
 To minimize: \textbf{sledgehammer} \textit{min} [\textit{remote\_waldmeister}] \\
 \phantom{To minimize: \textbf{sledgehammer}~}(\textit{hd.simps insert\_Nil}). \\[3\smallskipamount]
 %
 Sledgehammer: ``\textit{remote\_sine\_e}'' on goal: \\
 $[a] = [b] \,\Longrightarrow\, a = b$ \\
-Try this command: \textbf{by} (\textit{metis hd.simps}). \\
+Try this: \textbf{by} (\textit{metis hd.simps}). \\
 To minimize: \textbf{sledgehammer} \textit{min} [\textit{remote\_sine\_e}]~(\textit{hd.simps}). \\[3\smallskipamount]
 %
 Sledgehammer: ``\textit{remote\_z3}'' on goal: \\
 $[a] = [b] \,\Longrightarrow\, a = b$ \\
-Try this command: \textbf{by} (\textit{metis hd.simps}). \\
+Try this: \textbf{by} (\textit{metis hd.simps}). \\
 To minimize: \textbf{sledgehammer} \textit{min} [\textit{remote\_z3}]~(\textit{hd.simps}).
 \postw
 
diff -r e1172791ad0d -r e437d47f419f src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Fri May 27 10:30:08 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Fri May 27 10:30:08 2011 +0200
@@ -329,8 +329,8 @@
     Auto_Try => "Auto Sledgehammer (" ^ quote name ^ ") found a proof"
   | Try => "Sledgehammer (" ^ quote name ^ ") found a proof"
   | Normal => if blocking then quote name ^ " found a proof"
-              else "Try this command"
-  | Minimize => "Try this command"
+              else "Try this"
+  | Minimize => "Try this"
 
 val smt_triggers =
   Attrib.setup_config_bool @{binding sledgehammer_smt_triggers} (K true)
diff -r e1172791ad0d -r e437d47f419f src/HOL/Tools/try_methods.ML
--- a/src/HOL/Tools/try_methods.ML	Fri May 27 10:30:08 2011 +0200
+++ b/src/HOL/Tools/try_methods.ML	Fri May 27 10:30:08 2011 +0200
@@ -136,7 +136,7 @@
           (case mode of
              Auto_Try => "Auto Try Methods found a proof"
            | Try => "Try Methods found a proof"
-           | Normal => "Try this command") ^ ": " ^
+           | Normal => "Try this") ^ ": " ^
           Markup.markup Markup.sendback
               ((if nprems_of (#goal (Proof.goal st)) = 1 then "by"
                 else "apply") ^ " " ^ (s |> need_parens ? enclose "(" ")")) ^