1.1 --- a/doc-src/Sledgehammer/sledgehammer.tex	Wed Jul 28 18:35:15 2010 +0200
     1.2 +++ b/doc-src/Sledgehammer/sledgehammer.tex	Wed Jul 28 18:45:18 2010 +0200
     1.3 @@ -121,28 +121,33 @@
     1.4  \cite{sutcliffe-2000}, but if you want better performance you will need to
     1.5  install at least E and SPASS locally.
     1.6  
     1.7 -There are three main ways to install E and SPASS:
     1.8 +There are three main ways to install ATPs on your machine:
     1.9  
    1.10  \begin{enum}
    1.11  \item[$\bullet$] If you installed an official Isabelle package with everything
    1.12  inside, it should already include properly setup executables for E and SPASS,
    1.13 -ready to use.
    1.14 +ready to use.%
    1.15 +\footnote{Vampire's license prevents us from doing the same for this otherwise
    1.16 +wonderful tool.}
    1.17  
    1.18 -\item[$\bullet$] Otherwise, you can download the Isabelle-aware E and SPASS
    1.19 +\item[$\bullet$] Alternatively, you can download the Isabelle-aware E and SPASS
    1.20  binary packages from Isabelle's download page. Extract the archives, then add a
    1.21  line to your \texttt{\char`\~/.isabelle/etc/components} file with the absolute path to
    1.22 -E or SPASS. For example, if \texttt{\char`\~/.isabelle/etc/components} does not exist
    1.23 +E or SPASS. For example, if the \texttt{components} does not exist
    1.24  yet and you extracted SPASS to \texttt{/usr/local/spass-3.7}, create
    1.25 -the file \texttt{\char`\~/.isabelle/etc/components} with the single line
    1.26 +the \texttt{components} file with the single line
    1.27  
    1.28  \prew
    1.29  \texttt{/usr/local/spass-3.7}
    1.30  \postw
    1.31  
    1.32 -\item[$\bullet$] If you prefer to build E or SPASS yourself, feel free to do so
    1.33 -and set the environment variable \texttt{E\_HOME} or \texttt{SPASS\_HOME} to the
    1.34 -directory that contains the \texttt{eproof} or \texttt{SPASS} executable,
    1.35 -respectively.
    1.36 +in it.
    1.37 +
    1.38 +\item[$\bullet$] If you prefer to build E or SPASS yourself, or obtained a
    1.39 +Vampire executable from somewhere (e.g., \url{http://www.vprover.org/}),
    1.40 +set the environment variable \texttt{E\_HOME}, \texttt{SPASS\_HOME}, or
    1.41 +\texttt{VAMPIRE\_HOME} to the directory that contains the \texttt{eproof},
    1.42 +\texttt{SPASS}, or \texttt{vampire} executable.
    1.43  \end{enum}
    1.44  
    1.45  To check whether E and SPASS are installed, follow the example in
    1.46 @@ -176,29 +181,29 @@
    1.47  Sledgehammer: ATP ``\textit{e}'' for subgoal 1: \\
    1.48  $([a] = [b]) = (a = b)$ \\
    1.49  Try this command: \textbf{by} (\textit{metis hd.simps}). \\
    1.50 -To minimize the number of lemmas, try this command: \\
    1.51 +To minimize the number of lemmas, try this: \\
    1.52  \textbf{sledgehammer} \textit{minimize} [\textit{atp} = \textit{e}] (\textit{hd.simps}). \\[3\smallskipamount]
    1.53  %
    1.54  Sledgehammer: ATP ``\textit{spass}'' for subgoal 1: \\
    1.55  $([a] = [b]) = (a = b)$ \\
    1.56  Try this command: \textbf{by} (\textit{metis insert\_Nil last\_ConsL}). \\
    1.57 -To minimize the number of lemmas, try this command: \\
    1.58 +To minimize the number of lemmas, try this: \\
    1.59  \textbf{sledgehammer} \textit{minimize} [\textit{atp} = \textit{spass}] (\textit{insert\_Nil last\_ConsL}). \\[3\smallskipamount]
    1.60  %
    1.61  Sledgehammer: ATP ``\textit{remote\_vampire}'' for subgoal 1: \\
    1.62  $([a] = [b]) = (a = b)$ \\
    1.63  Try this command: \textbf{by} (\textit{metis One\_nat\_def\_raw empty\_replicate} \\
    1.64  \phantom{Try this command: \textbf{by} (\textit{metis~}}\textit{insert\_Nil last\_ConsL replicate\_Suc}). \\
    1.65 -To minimize the number of lemmas, try this command: \\
    1.66 +To minimize the number of lemmas, try this: \\
    1.67  \textbf{sledgehammer} \textit{minimize} [\textit{atp} = \textit{remote\_vampire}] \\
    1.68  \phantom{\textbf{sledgehammer}~}(\textit{One\_nat\_def\_raw empty\_replicate insert\_Nil} \\
    1.69  \phantom{\textbf{sledgehammer}~(}\textit{last\_ConsL replicate\_Suc}).
    1.70  \postw
    1.71  
    1.72  Sledgehammer ran E, SPASS, and the remote version of Vampire in parallel. If E
    1.73 -and SPASS are not installed (\S\ref{installation}), you will see references to
    1.74 -their remote American cousins \textit{remote\_e} and \textit{remote\_spass}
    1.75 -instead of \textit{e} and \textit{spass}.
    1.76 +is not installed (\S\ref{installation}), you will see references to
    1.77 +its remote American cousin \textit{remote\_e} instead of
    1.78 +\textit{e}; and if SPASS is not installed, it will not appear in the output.
    1.79  
    1.80  Based on each ATP proof, Sledgehammer gives a one-liner proof that uses the
    1.81  \textit{metis} method. You can click them and insert them into the theory text.
    1.82 @@ -377,9 +382,6 @@
    1.83  \item[$\bullet$] \textbf{\textit{remote\_e}:} The remote version of E executes
    1.84  on Geoff Sutcliffe's Miami servers \cite{sutcliffe-2000}.
    1.85  
    1.86 -\item[$\bullet$] \textbf{\textit{remote\_spass}:} The remote version of SPASS
    1.87 -executes on Geoff Sutcliffe's Miami servers.
    1.88 -
    1.89  \item[$\bullet$] \textbf{\textit{remote\_vampire}:} The remote version of
    1.90  Vampire executes on Geoff Sutcliffe's Miami servers. Version 9 is used.
    1.91