# 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