src/Doc/Sledgehammer/document/root.tex

 contains the \texttt{runepar.pl} script and the \texttt{eprover} and
 \texttt{epclextract} executables, or use the prebuilt E package from \download.
 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
 directory that contains the \texttt{iprover} and \texttt{vclausify\_rel}
 executables. Sledgehammer has been tested with version 0.99.