src/Doc/Sledgehammer/document/root.tex

 Sledgehammer panel in Isabelle/jEdit. Sledgehammer produces the following output
 after a few seconds:
 
 \prew
 \slshape
-Sledgehammer: ``\textit{cvc4\/}'' \\
-Try this: \textbf{by} (\textit{metis last\_ConsL}) (64 ms). \\[3\smallskipamount]
-%
-Sledgehammer: ``\textit{z3\/}'' \\
-Try this: \textbf{by} (\textit{metis list.inject}) (20 ms). \\[3\smallskipamount]
-%
-Sledgehammer: ``\textit{spass\/}'' \\
-Try this: \textbf{by} (\textit{metis list.inject}) (17 ms). \\[3\smallskipamount]
-%
-Sledgehammer: ``\textit{e\/}'' \\
-Try this: \textbf{by} (\textit{metis hd.simps}) (14 ms). \\[3\smallskipamount]
+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).
+%
 \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
 provers might be missing or present with a \textit{remote\_} prefix.