--- a/src/Doc/Sledgehammer/document/root.tex Tue May 22 11:08:37 2018 +0200
+++ b/src/Doc/Sledgehammer/document/root.tex Tue May 22 17:15:02 2018 +0200
@@ -768,6 +768,10 @@
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 \texttt{IPROVER\_HOME} to the