--- a/doc-src/Sledgehammer/sledgehammer.tex Fri Feb 24 11:23:32 2012 +0100
+++ b/doc-src/Sledgehammer/sledgehammer.tex Fri Feb 24 11:23:33 2012 +0100
@@ -465,7 +465,7 @@
but the proof is, for technical reasons, beyond \textit{metis}'s power. You can
then try again with the \textit{strict} option (\S\ref{problem-encoding}).
-If the goal is actually unprovable are you did not specify an unsound encoding
+If the goal is actually unprovable and you did not specify an unsound encoding
using \textit{type\_enc} (\S\ref{problem-encoding}), this is a bug, and you are
strongly encouraged to report this to the author at \authoremail.
@@ -483,7 +483,7 @@
Earlier versions of Sledgehammer often suggested unsound proofs---either proofs
of nontheorems or simply proofs that rely on type-unsound inferences. This
-is a thing of the pass, unless you explicitly specify an unsound encoding
+is a thing of the past, unless you explicitly specify an unsound encoding
using \textit{type\_enc} (\S\ref{problem-encoding}).
%
Officially, the only form of ``unsoundness'' that lurks in the sound
@@ -564,7 +564,7 @@
In addition, some provers (e.g., Yices) do not provide proofs or sometimes
produce incomplete proofs. The minimizer is then invoked to find out which facts
-are actually needed from the (large) set of facts that was initinally given to
+are actually needed from the (large) set of facts that was initially given to
the prover. Finally, if a prover returns a proof with lots of facts, the
minimizer is invoked automatically since Metis would be unlikely to re-find the
proof.
@@ -845,7 +845,7 @@
\item[\labelitemi] \textbf{\textit{remote\_e\_sine}:} E-SInE is a metaprover
developed by Kry\v stof Hoder \cite{sine} based on E. The remote version of
-SInE runs on Geoff Sutcliffe's Miami servers.
+E-SInE runs on Geoff Sutcliffe's Miami servers.
\item[\labelitemi] \textbf{\textit{remote\_e\_tofof}:} E-ToFoF is a metaprover
developed by Geoff Sutcliffe \cite{tofof} based on E running on his Miami
@@ -863,9 +863,6 @@
remote version of iProver-Eq runs on Geoff Sutcliffe's Miami servers
\cite{sutcliffe-2000}.
-The remote version of LEO-II
-runs on Geoff Sutcliffe's Miami servers \cite{sutcliffe-2000}.
-
\item[\labelitemi] \textbf{\textit{remote\_leo2}:} The remote version of LEO-II
runs on Geoff Sutcliffe's Miami servers \cite{sutcliffe-2000}.