# HG changeset patch
# User blanchet
# Date 1307386944 -7200
# Node ID 558313900b44c471c622537994ffd8f94584b1a0
# Parent  4e850b2c1f5c5fd266f61f109fb9af011efeb59b
updated Sledgehammer message

diff -r 4e850b2c1f5c -r 558313900b44 doc-src/Nitpick/nitpick.tex
--- a/doc-src/Nitpick/nitpick.tex	Mon Jun 06 20:56:06 2011 +0200
+++ b/doc-src/Nitpick/nitpick.tex	Mon Jun 06 21:02:24 2011 +0200
@@ -354,10 +354,10 @@
 
 \prew
 \textbf{sledgehammer} \\[2\smallskipamount]
-{\slshape Sledgehammer: external prover ``$e$'' for subgoal 1: \\
+{\slshape Sledgehammer: ``$e$'' on goal: \\
 $\exists{!}x.\; P~x\,\Longrightarrow\, P~(\hbox{\slshape THE}~y.\; P~y)$ \\
-Try this command: \textrm{apply}~(\textit{metis~the\_equality})} \\[2\smallskipamount]
-\textbf{apply}~(\textit{metis~the\_equality\/}) \nopagebreak \\[2\smallskipamount]
+Try this: \textrm{apply}~(\textit{metis~theI}) (21 ms).} \\[2\smallskipamount]
+\textbf{by}~(\textit{metis~theI\/}) \nopagebreak \\[2\smallskipamount]
 {\slshape No subgoals!}% \\[2\smallskipamount]
 %\textbf{done}
 \postw