1.1 --- a/doc-src/Nitpick/nitpick.tex	Mon Jun 06 20:56:06 2011 +0200
     1.2 +++ b/doc-src/Nitpick/nitpick.tex	Mon Jun 06 21:02:24 2011 +0200
     1.3 @@ -354,10 +354,10 @@
     1.4  
     1.5  \prew
     1.6  \textbf{sledgehammer} \\[2\smallskipamount]
     1.7 -{\slshape Sledgehammer: external prover ``$e$'' for subgoal 1: \\
     1.8 +{\slshape Sledgehammer: ``$e$'' on goal: \\
     1.9  $\exists{!}x.\; P~x\,\Longrightarrow\, P~(\hbox{\slshape THE}~y.\; P~y)$ \\
    1.10 -Try this command: \textrm{apply}~(\textit{metis~the\_equality})} \\[2\smallskipamount]
    1.11 -\textbf{apply}~(\textit{metis~the\_equality\/}) \nopagebreak \\[2\smallskipamount]
    1.12 +Try this: \textrm{apply}~(\textit{metis~theI}) (21 ms).} \\[2\smallskipamount]
    1.13 +\textbf{by}~(\textit{metis~theI\/}) \nopagebreak \\[2\smallskipamount]
    1.14  {\slshape No subgoals!}% \\[2\smallskipamount]
    1.15  %\textbf{done}
    1.16  \postw