src/Doc/Sledgehammer/document/root.tex

 after a few seconds:
 
 \prew
 \slshape
 Proof found\ldots \\
-``\textit{e\/}'': Try this: \textbf{by} \textit{simp} (0.3 ms). \\
-%
-``\textit{cvc4\/}'': Try this: \textbf{by} \textit{simp} (0.4 ms). \\
-%
-``\textit{z3\/}'': Try this: \textbf{by} \textit{simp} (0.5 ms). \\
-%
-``\textit{spass\/}'': Try this: \textbf{by} \textit{simp} (0.3 ms).
+``\textit{e\/}'': Try this: \textbf{by} \textit{simp} (0.3 ms) \\
+%
+``\textit{cvc4\/}'': Try this: \textbf{by} \textit{simp} (0.4 ms) \\
+%
+``\textit{z3\/}'': Try this: \textbf{by} \textit{simp} (0.5 ms) \\
+%
+``\textit{spass\/}'': Try this: \textbf{by} \textit{simp} (0.3 ms)
 %
 \postw
 
 Sledgehammer ran CVC4, E, SPASS, and Z3 in parallel. Depending on which
 provers are installed and how many processor cores are available, some of the

 
 Incidentally, if you ever see warnings such as
 
 \prew
 \slshape
-Metis: Falling back on ``\textit{metis} (\textit{full\_types})''.
+Metis: Falling back on ``\textit{metis} (\textit{full\_types})''
 \postw
 
 for a successful \textit{metis} proof, you can advantageously pass the
 \textit{full\_types} option to \textit{metis} directly.
 

 (\S\ref{mode-of-operation}).
 
 \point{A strange error occurred---what should I do?}
 
 Sledgehammer tries to give informative error messages. Please report any strange
-error to the author at \authoremail. This applies doubly if you get the message
-
-\prew
-\slshape
-The prover derived ``\textit{False}'' using ``\textit{foo\/}'',
-``\textit{bar\/}'', and ``\textit{baz\/}''.
-This could be due to inconsistent axioms (including ``\textbf{sorry}''s) or to
-a bug in Sledgehammer. If the problem persists, please contact the
-Isabelle developers.
-\postw
+error to the author at \authoremail.
 
 \point{Auto can solve it---why not Sledgehammer?}
 
 Problems can be easy for \textit{auto} and difficult for automatic provers, but
 the reverse is also true, so do not be discouraged if your first attempts fail.