# HG changeset patch
# User blanchet
# Date 1632734396 -7200
# Node ID ba30067b7259630f48c1d615ed4caa6feac8ec05
# Parent  d1185d02aef5ca0ca86c05b6adfecbe4df837267
tuned docs

diff -r d1185d02aef5 -r ba30067b7259 src/Doc/Sledgehammer/document/root.tex
--- 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