--- a/src/Doc/Sledgehammer/document/root.tex Thu Oct 08 17:46:03 2020 +0200
+++ b/src/Doc/Sledgehammer/document/root.tex Thu Oct 08 17:47:35 2020 +0200
@@ -773,10 +773,6 @@
Be aware that E-Par is experimental software. It has been known to generate
zombie processes. Use at your own risks.
-\item[\labelitemi] \textbf{\textit{ehoh}:} Ehoh is an experimental version of
-E that supports a $\lambda$-free fragment of higher-order logic. Use at your
-own risks.
-
\item[\labelitemi] \textbf{\textit{iprover}:} iProver is a pure
instantiation-based prover developed by Konstantin Korovin
\cite{korovin-2009}. To use iProver, set the environment variable