# HG changeset patch
# User blanchet
# Date 1391597276 -3600
# Node ID 5f5104069b3339d9a1448e3d82e69116587b895a
# Parent  fa079fd40db8633abd5269f8adc54b62ef2dffb8
agsyHOL is also called AgsyHOL by Lindblad himself, so let's follow this convention

diff -r fa079fd40db8 -r 5f5104069b33 src/Doc/Sledgehammer/document/root.tex
--- a/src/Doc/Sledgehammer/document/root.tex	Wed Feb 05 11:37:32 2014 +0100
+++ b/src/Doc/Sledgehammer/document/root.tex	Wed Feb 05 11:47:56 2014 +0100
@@ -100,7 +100,7 @@
 between instantiation-based ATPs (such as iProver and iProver-Eq) and SMT
 solvers.}
 %
-The supported ATPs are agsyHOL \cite{agsyHOL}, Alt-Ergo \cite{alt-ergo}, E
+The supported ATPs are AgsyHOL \cite{agsyHOL}, Alt-Ergo \cite{alt-ergo}, E
 \cite{schulz-2002}, E-SInE \cite{sine}, E-ToFoF \cite{tofof}, iProver
 \cite{korovin-2009}, iProver-Eq \cite{korovin-sticksel-2010}, LEO-II
 \cite{leo2}, Satallax \cite{satallax}, SNARK \cite{snark}, SPASS
@@ -150,8 +150,8 @@
 Sledgehammer is part of Isabelle, so you do not need to install it. However, it
 relies on third-party automatic provers (ATPs and SMT solvers).
 
-Among the ATPs, agsyHOL, Alt-Ergo, E, LEO-II, Satallax, SPASS, and Vampire can
-be run locally; in addition, agsyHOL, E, E-SInE, E-ToFoF, iProver, iProver-Eq,
+Among the ATPs, AgsyHOL, Alt-Ergo, E, LEO-II, Satallax, SPASS, and Vampire can
+be run locally; in addition, AgsyHOL, E, E-SInE, E-ToFoF, iProver, iProver-Eq,
 LEO-II, Satallax, SNARK, Vampire, and Waldmeister are available remotely via
 System\-On\-TPTP \cite{sutcliffe-2000}. If you want better performance, you
 should at least install E and SPASS locally.
@@ -191,7 +191,7 @@
 
 in it.
 
-\item[\labelitemi] If you prefer to build agsyHOL, Alt-Ergo, E, LEO-II,
+\item[\labelitemi] If you prefer to build AgsyHOL, Alt-Ergo, E, LEO-II,
 Satallax, or SPASS manually, or found a Vampire executable somewhere (e.g.,
 \url{http://www.vprover.org/}), set the environment variable
 \texttt{AGSYHOL\_HOME}, \texttt{E\_HOME}, \texttt{LEO2\_HOME},
@@ -202,7 +202,7 @@
 for Alt-Ergo, set the
 environment variable \texttt{WHY3\_HOME} to the directory that contains the
 \texttt{why3} executable.
-Sledgehammer has been tested with agsyHOL 1.0, Alt-Ergo 0.95.1, E 1.0 to 1.8,
+Sledgehammer has been tested with AgsyHOL 1.0, Alt-Ergo 0.95.1, E 1.0 to 1.8,
 LEO-II 1.3.4, Satallax 2.2 to 2.7, SPASS 3.8ds, and Vampire 0.6 to 3.0.%
 \footnote{Following the rewrite of Vampire, the counter for version numbers was
 reset to 0; hence the (new) Vampire versions 0.6, 1.0, 1.8, 2.6, and 3.0 are more
@@ -816,9 +816,9 @@
 
 \begin{sloppy}
 \begin{enum}
-\item[\labelitemi] \textbf{\textit{agsyHOL}:} agsyHOL is an automatic
+\item[\labelitemi] \textbf{\textit{agsyhol}:} AgsyHOL is an automatic
 higher-order prover developed by Fredrik Lindblad \cite{agsyHOL},
-with support for the TPTP typed higher-order syntax (THF0). To use agsyHOL, set
+with support for the TPTP typed higher-order syntax (THF0). To use AgsyHOL, set
 the environment variable \texttt{AGSYHOL\_HOME} to the directory that contains
 the \texttt{agsyHOL} executable. Sledgehammer has been tested with version 1.0.
 
@@ -922,7 +922,7 @@
 
 \begin{enum}
 \item[\labelitemi] \textbf{\textit{remote\_agsyhol}:} The remote version of
-agsyHOL runs on Geoff Sutcliffe's Miami servers \cite{sutcliffe-2000}.
+AgsyHOL runs on Geoff Sutcliffe's Miami servers \cite{sutcliffe-2000}.
 
 \item[\labelitemi] \textbf{\textit{remote\_e}:} The remote version of E runs
 on Geoff Sutcliffe's Miami servers \cite{sutcliffe-2000}.