# HG changeset patch
# User blanchet
# Date 1288116753 -7200
# Node ID aff7d1471b620b44c55bc37e86a0e144cddd3208
# Parent  ce996440ff2b2959d0a8ed308a57505301fcc321
"Nitpick" -> "Sledgehammer";
reparagraphing

diff -r ce996440ff2b -r aff7d1471b62 doc-src/Sledgehammer/sledgehammer.tex
--- a/doc-src/Sledgehammer/sledgehammer.tex	Tue Oct 26 20:09:38 2010 +0200
+++ b/doc-src/Sledgehammer/sledgehammer.tex	Tue Oct 26 20:12:33 2010 +0200
@@ -141,10 +141,10 @@
 
 \item[$\bullet$] Alternatively, you can download the Isabelle-aware E and SPASS
 binary packages from Isabelle's download page. Extract the archives, then add a
-line to your \texttt{\char`\~/.isabelle/etc/components} file with the absolute path to
-E or SPASS. For example, if the \texttt{components} does not exist
-yet and you extracted SPASS to \texttt{/usr/local/spass-3.7}, create
-the \texttt{components} file with the single line
+line to your \texttt{\char`\~/.isabelle/etc/components} file with the absolute
+path to E or SPASS. For example, if the \texttt{components} does not exist yet
+and you extracted SPASS to \texttt{/usr/local/spass-3.7}, create the
+\texttt{components} file with the single line
 
 \prew
 \texttt{/usr/local/spass-3.7}
@@ -223,13 +223,7 @@
 $([a] = [b]) = (a = b)$ \\
 Try this command: \textbf{by} (\textit{metis hd.simps}) \\
 To minimize the number of lemmas, try this: \\
-\textbf{sledgehammer} \textit{minimize} [\textit{prover} = \textit{remote\_sine\_e}]~(\textit{hd.simps}). \\[3\smallskipamount]
-%
-Sledgehammer: ``\textit{smt}'' for subgoal 1: \\
-$([a] = [b]) = (a = b)$ \\
-Try this command: \textbf{by} (\textit{smt hd.simps}) \\
-To minimize the number of lemmas, try this: \\
-\textbf{sledgehammer} \textit{minimize} [\textit{prover} = \textit{smt}]~(\textit{hd.simps}).
+\textbf{sledgehammer} \textit{minimize} [\textit{prover} = \textit{remote\_sine\_e}]~(\textit{hd.simps}).
 \postw
 
 Sledgehammer ran E, SPASS, Vampire, SInE-E, and the \textit{smt} proof method in
@@ -290,21 +284,21 @@
 In the general syntax, the \textit{subcommand} may be any of the following:
 
 \begin{enum}
-\item[$\bullet$] \textbf{\textit{run} (the default):} Runs Sledgehammer on subgoal number
-\textit{num} (1 by default), with the given options and facts.
+\item[$\bullet$] \textbf{\textit{run} (the default):} Runs Sledgehammer on
+subgoal number \textit{num} (1 by default), with the given options and facts.
 
 \item[$\bullet$] \textbf{\textit{minimize}:} Attempts to minimize the provided facts
 (specified in the \textit{facts\_override} argument) to obtain a simpler proof
 involving fewer facts. The options and goal number are as for \textit{run}.
 
-\item[$\bullet$] \textbf{\textit{messages}:} Redisplays recent messages issued by
-Sledgehammer. This allows you to examine results that might have been lost due
-to Sledgehammer's asynchronous nature. The \textit{num} argument specifies a
+\item[$\bullet$] \textbf{\textit{messages}:} Redisplays recent messages issued
+by Sledgehammer. This allows you to examine results that might have been lost
+due to Sledgehammer's asynchronous nature. The \textit{num} argument specifies a
 limit on the number of messages to display (5 by default).
 
-\item[$\bullet$] \textbf{\textit{available\_provers}:} Prints the list of installed provers.
-See \S\ref{installation} and \S\ref{mode-of-operation} for more information on
-how to install automatic provers.
+\item[$\bullet$] \textbf{\textit{available\_provers}:} Prints the list of
+installed provers. See \S\ref{installation} and \S\ref{mode-of-operation} for
+more information on how to install automatic provers.
 
 \item[$\bullet$] \textbf{\textit{running\_provers}:} Prints information about
 currently running automatic provers, including elapsed runtime and remaining
@@ -380,10 +374,12 @@
 \begin{enum}
 \item[$\bullet$] \qtybf{string}: A string.
 \item[$\bullet$] \qtybf{bool\/}: \textit{true} or \textit{false}.
-\item[$\bullet$] \qtybf{bool\_or\_smart\/}: \textit{true}, \textit{false}, or \textit{smart}.
+\item[$\bullet$] \qtybf{bool\_or\_smart\/}: \textit{true}, \textit{false}, or
+\textit{smart}.
 \item[$\bullet$] \qtybf{int\/}: An integer.
 \item[$\bullet$] \qtybf{int\_or\_smart\/}: An integer or \textit{smart}.
-\item[$\bullet$] \qtybf{time}: An integer followed by $\textit{min}$ (minutes), $s$ (seconds), or \textit{ms}
+\item[$\bullet$] \qtybf{time}: An integer followed by $\textit{min}$ (minutes),
+$s$ (seconds), or \textit{ms}
 (milliseconds), or the keyword \textit{none} ($\infty$ years).
 \end{enum}
 
@@ -531,9 +527,9 @@
 Specifies whether the \textbf{sledgehammer} command should explain what it does.
 
 \opfalse{debug}{no\_debug}
-Specifies whether Nitpick should display additional debugging information beyond
-what \textit{verbose} already displays. Enabling \textit{debug} also enables
-\textit{verbose} behind the scenes.
+Specifies whether Sledgehammer should display additional debugging information
+beyond what \textit{verbose} already displays. Enabling \textit{debug} also
+enables \textit{verbose} behind the scenes.
 
 \nopagebreak
 {\small See also \textit{overlord} (\S\ref{mode-of-operation}).}
@@ -559,9 +555,11 @@
 Specifies the expected outcome, which must be one of the following:
 
 \begin{enum}
-\item[$\bullet$] \textbf{\textit{some}:} Sledgehammer found a (potentially unsound) proof.
+\item[$\bullet$] \textbf{\textit{some}:} Sledgehammer found a (potentially
+unsound) proof.
 \item[$\bullet$] \textbf{\textit{none}:} Sledgehammer found no proof.
-\item[$\bullet$] \textbf{\textit{unknown}:} Sledgehammer encountered some problem.
+\item[$\bullet$] \textbf{\textit{unknown}:} Sledgehammer encountered some
+problem.
 \end{enum}
 
 Sledgehammer emits an error (if \textit{blocking} is enabled) or a warning