diff -r dd5874e4553f -r af9cdb4989c7 src/Doc/Sledgehammer/document/root.tex --- a/src/Doc/Sledgehammer/document/root.tex Mon Dec 09 04:03:30 2013 +0100 +++ b/src/Doc/Sledgehammer/document/root.tex Mon Dec 09 04:03:30 2013 +0100 @@ -850,11 +850,13 @@ that contains the \texttt{emales.py} script. Sledgehammer has been tested with version 1.1. -\item[\labelitemi] \textbf{\textit{e\_par}:} E-Par is a metaprover developed -by Josef Urban that implements strategy scheduling on top of E. To use -E-Par, set the environment variable \texttt{E\_HOME} to the directory -that contains the \texttt{runepar.pl} script and the \texttt{eprover} and +\item[\labelitemi] \textbf{\textit{e\_par}:} E-Par is an experimental metaprover +developed by Josef Urban that implements strategy scheduling on top of E. To use +E-Par, set the environment variable \texttt{E\_HOME} to the directory that +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{iprover}:} iProver is a pure instantiation-based prover developed by Konstantin Korovin \cite{korovin-2009}.