1.1 --- a/doc-src/Sledgehammer/sledgehammer.tex	Fri May 27 10:30:08 2011 +0200
     1.2 +++ b/doc-src/Sledgehammer/sledgehammer.tex	Fri May 27 10:30:08 2011 +0200
     1.3 @@ -249,33 +249,33 @@
     1.4  \slshape
     1.5  Sledgehammer: ``\textit{e}'' on goal: \\
     1.6  $[a] = [b] \,\Longrightarrow\, a = b$ \\
     1.7 -Try this command: \textbf{by} (\textit{metis last\_ConsL}). \\
     1.8 +Try this: \textbf{by} (\textit{metis last\_ConsL}). \\
     1.9  To minimize: \textbf{sledgehammer} \textit{min} [\textit{e}] (\textit{last\_ConsL}). \\[3\smallskipamount]
    1.10  %
    1.11  Sledgehammer: ``\textit{vampire}'' on goal: \\
    1.12  $[a] = [b] \,\Longrightarrow\, a = b$ \\
    1.13 -Try this command: \textbf{by} (\textit{metis hd.simps}). \\
    1.14 +Try this: \textbf{by} (\textit{metis hd.simps}). \\
    1.15  To minimize: \textbf{sledgehammer} \textit{min} [\textit{vampire}] (\textit{hd.simps}). \\[3\smallskipamount]
    1.16  %
    1.17  Sledgehammer: ``\textit{spass}'' on goal: \\
    1.18  $[a] = [b] \,\Longrightarrow\, a = b$ \\
    1.19 -Try this command: \textbf{by} (\textit{metis list.inject}). \\
    1.20 +Try this: \textbf{by} (\textit{metis list.inject}). \\
    1.21  To minimize: \textbf{sledgehammer} \textit{min} [\textit{spass}]~(\textit{list.inject}). \\[3\smallskipamount]
    1.22  %
    1.23  Sledgehammer: ``\textit{remote\_waldmeister}'' on goal: \\
    1.24  $[a] = [b] \,\Longrightarrow\, a = b$ \\
    1.25 -Try this command: \textbf{by} (\textit{metis hd.simps insert\_Nil}). \\
    1.26 +Try this: \textbf{by} (\textit{metis hd.simps insert\_Nil}). \\
    1.27  To minimize: \textbf{sledgehammer} \textit{min} [\textit{remote\_waldmeister}] \\
    1.28  \phantom{To minimize: \textbf{sledgehammer}~}(\textit{hd.simps insert\_Nil}). \\[3\smallskipamount]
    1.29  %
    1.30  Sledgehammer: ``\textit{remote\_sine\_e}'' on goal: \\
    1.31  $[a] = [b] \,\Longrightarrow\, a = b$ \\
    1.32 -Try this command: \textbf{by} (\textit{metis hd.simps}). \\
    1.33 +Try this: \textbf{by} (\textit{metis hd.simps}). \\
    1.34  To minimize: \textbf{sledgehammer} \textit{min} [\textit{remote\_sine\_e}]~(\textit{hd.simps}). \\[3\smallskipamount]
    1.35  %
    1.36  Sledgehammer: ``\textit{remote\_z3}'' on goal: \\
    1.37  $[a] = [b] \,\Longrightarrow\, a = b$ \\
    1.38 -Try this command: \textbf{by} (\textit{metis hd.simps}). \\
    1.39 +Try this: \textbf{by} (\textit{metis hd.simps}). \\
    1.40  To minimize: \textbf{sledgehammer} \textit{min} [\textit{remote\_z3}]~(\textit{hd.simps}).
    1.41  \postw
    1.42  

     2.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Fri May 27 10:30:08 2011 +0200
     2.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Fri May 27 10:30:08 2011 +0200
     2.3 @@ -329,8 +329,8 @@
     2.4      Auto_Try => "Auto Sledgehammer (" ^ quote name ^ ") found a proof"
     2.5    | Try => "Sledgehammer (" ^ quote name ^ ") found a proof"
     2.6    | Normal => if blocking then quote name ^ " found a proof"
     2.7 -              else "Try this command"
     2.8 -  | Minimize => "Try this command"
     2.9 +              else "Try this"
    2.10 +  | Minimize => "Try this"
    2.11  
    2.12  val smt_triggers =
    2.13    Attrib.setup_config_bool @{binding sledgehammer_smt_triggers} (K true)

     3.1 --- a/src/HOL/Tools/try_methods.ML	Fri May 27 10:30:08 2011 +0200
     3.2 +++ b/src/HOL/Tools/try_methods.ML	Fri May 27 10:30:08 2011 +0200
     3.3 @@ -136,7 +136,7 @@
     3.4            (case mode of
     3.5               Auto_Try => "Auto Try Methods found a proof"
     3.6             | Try => "Try Methods found a proof"
     3.7 -           | Normal => "Try this command") ^ ": " ^
     3.8 +           | Normal => "Try this") ^ ": " ^
     3.9            Markup.markup Markup.sendback
    3.10                ((if nprems_of (#goal (Proof.goal st)) = 1 then "by"
    3.11                  else "apply") ^ " " ^ (s |> need_parens ? enclose "(" ")")) ^