# HG changeset patch
# User blanchet
# Date 1330079013 -3600
# Node ID 622691cec7c30c85dc30c4eaf19cfc767f47537a
# Parent  d0ef1d1562d77e09b1702aad9cad2373ccc05c78
doc fixes (thanks to Nik)

diff -r d0ef1d1562d7 -r 622691cec7c3 doc-src/Sledgehammer/sledgehammer.tex
--- 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}.