diff -r 03b995c21878 -r bdb5fd0050f5 src/Doc/Sledgehammer/document/root.tex
--- a/src/Doc/Sledgehammer/document/root.tex	Mon Mar 28 12:05:47 2016 +0200
+++ b/src/Doc/Sledgehammer/document/root.tex	Mon Mar 28 12:05:47 2016 +0200
@@ -260,17 +260,15 @@
 
 \prew
 \slshape
-Sledgehammer: ``\textit{cvc4\/}'' \\
-Try this: \textbf{by} (\textit{metis last\_ConsL}) (64 ms). \\[3\smallskipamount]
+Proof found\ldots \\
+``\textit{e\/}'': Try this: \textbf{by} \textit{simp} (0.3 ms). \\
 %
-Sledgehammer: ``\textit{z3\/}'' \\
-Try this: \textbf{by} (\textit{metis list.inject}) (20 ms). \\[3\smallskipamount]
+``\textit{cvc4\/}'': Try this: \textbf{by} \textit{simp} (0.4 ms). \\
 %
-Sledgehammer: ``\textit{spass\/}'' \\
-Try this: \textbf{by} (\textit{metis list.inject}) (17 ms). \\[3\smallskipamount]
+``\textit{z3\/}'': Try this: \textbf{by} \textit{simp} (0.5 ms). \\
 %
-Sledgehammer: ``\textit{e\/}'' \\
-Try this: \textbf{by} (\textit{metis hd.simps}) (14 ms). \\[3\smallskipamount]
+``\textit{spass\/}'': Try this: \textbf{by} \textit{simp} (0.3 ms).
+%
 \postw
 
 Sledgehammer ran CVC4, E, SPASS, and Z3 in parallel. Depending on which