--- a/src/Doc/Sledgehammer/document/root.tex Wed Sep 22 12:25:09 2021 +0200
+++ b/src/Doc/Sledgehammer/document/root.tex Wed Sep 22 12:41:40 2021 +0200
@@ -159,9 +159,7 @@
\begin{enum}
\item[\labelitemi] If you installed an official Isabelle package, it should
already include properly set up executables for CVC4, E, SPASS, Vampire, veriT,
-and Z3, ready to use. To use Vampire, you must confirm that you are a
-noncommercial user, as indicated by the message that is displayed when
-Sledgehammer is invoked the first time.
+and Z3, ready to use.
\item[\labelitemi] Alternatively, you can download the Isabelle-aware CVC4, E,
SPASS, Vampire, veriT, and Z3 binary packages from \download. Extract the