1.1 --- a/src/Doc/Sledgehammer/document/root.tex	Thu Jan 17 14:02:25 2013 +0100
     1.2 +++ b/src/Doc/Sledgehammer/document/root.tex	Thu Jan 17 14:06:14 2013 +0100
     1.3 @@ -12,7 +12,7 @@
     1.4  %\usepackage[scaled=.85]{beramono}
     1.5  \usepackage{isabelle,iman,pdfsetup}
     1.6  
     1.7 -\newcommand\download{\url{http://www21.in.tum.de/~blanchet/\#software}}
     1.8 +\newcommand\download{\url{http://isabelle.in.tum.de/components/}}
     1.9  
    1.10  \def\qty#1{\ensuremath{\left<\mathit{#1\/}\right>}}
    1.11  \def\qtybf#1{$\mathbf{\left<\textbf{\textit{#1\/}}\right>}$}
    1.12 @@ -865,6 +865,12 @@
    1.13  that contains the \texttt{emales.py} script. Sledgehammer has been tested with
    1.14  version 1.1.
    1.15  
    1.16 +\item[\labelitemi] \textbf{\textit{e\_par}:} E-Par is a metaprover developed
    1.17 +by Josef Urban that implements strategy scheduling on top of E. To use
    1.18 +E-Par, set the environment variable \texttt{E\_HOME} to the directory
    1.19 +that contains the \texttt{runepar.pl} script and the \texttt{eprover} and
    1.20 +\texttt{epclextract} executables, or use the prebuilt E package from \download.
    1.21 +
    1.22  \item[\labelitemi] \textbf{\textit{iprover}:} iProver is a pure
    1.23  instantiation-based prover developed by Konstantin Korovin \cite{korovin-2009}.
    1.24  To use iProver, set the environment variable \texttt{IPROVER\_HOME} to the