--- a/src/Doc/Sledgehammer/document/root.tex Sun Sep 26 20:13:28 2021 +0200
+++ b/src/Doc/Sledgehammer/document/root.tex Mon Sep 27 11:19:56 2021 +0200
@@ -235,13 +235,13 @@
%
``\textit{z3\/}'': Try this: \textbf{by} \textit{simp} (0.5 ms) \\
%
-``\textit{spass\/}'': Try this: \textbf{by} \textit{simp} (0.3 ms)
+``\textit{vampire\/}'': 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.
+Sledgehammer ran CVC4, E, Vampire, and Z3 in parallel. This list may vary
+depending on which provers are installed and how many processor cores are
+available.
For each successful prover, Sledgehammer gives a one-line Isabelle proof. Rough
timings are shown in parentheses, indicating how fast the call is. You can