# HG changeset patch
# User blanchet
# Date 1307429903 -7200
# Node ID 443708f05bb2b700ecebe8b0ab24c649ce8a285c
# Parent  2ed2f092e990084e18102fa650761169606a7d5e
documentation tweaks

diff -r 2ed2f092e990 -r 443708f05bb2 doc-src/Sledgehammer/sledgehammer.tex
--- a/doc-src/Sledgehammer/sledgehammer.tex	Tue Jun 07 08:52:35 2011 +0200
+++ b/doc-src/Sledgehammer/sledgehammer.tex	Tue Jun 07 08:58:23 2011 +0200
@@ -495,7 +495,8 @@
 set the \textit{isar\_shrink\_factor} option (\S\ref{output-format}) to a larger
 value or to try several provers and keep the nicest-looking proof.
 
-\point{What is the \textit{full\_types}/\textit{no\_types} argument to Metis?}
+\point{What are the \textit{full\_types} and \textit{no\_types} arguments to
+Metis?}
 
 The \textit{metis}~(\textit{full\_types}) proof method is the fully-typed
 version of Metis. It is somewhat slower than \textit{metis}, but the proof
@@ -510,7 +511,12 @@
 actually work and to display timing information. This can be configured using
 the \textit{preplay\_timeout} option (\S\ref{timeouts}).)
 
-If you see the warning
+At the other end of the soundness spectrum, \textit{metis} (\textit{no\_types})
+uses no type information at all during the proof search, which is more efficient
+but often fails. Calls to \textit{metis} (\textit{no\_types}) are occasionally
+generated by Sledgehammer.
+
+Incidentally, if you see the warning
 
 \prew
 \slshape
@@ -520,11 +526,6 @@
 in a successful Metis proof, you can advantageously pass the
 \textit{full\_types} option to \textit{metis} directly.
 
-At the other end of the soundness spectrum, \textit{metis} (\textit{no\_types})
-uses no type information at all during the proof search, which is more efficient
-but often fails. Calls to \textit{metis} (\textit{no\_types}) are occasionally
-generated by Sledgehammer.
-
 \point{Are generated proofs minimal?}
 
 Automatic provers frequently use many more facts than are necessary.
@@ -534,11 +535,11 @@
 improves Metis's speed and success rate, while also removing superfluous clutter
 from the proof scripts.
 
-In earlier versions of Sledgehammer, generated proofs were accompanied by a
-suggestion to invoke the minimization tool. This step is now performed
-implicitly if it can be done in a reasonable amount of time (something that can
-be guessed from the number of facts in the original proof and the time it took
-to find it or replay it).
+In earlier versions of Sledgehammer, generated proofs were systematically
+accompanied by a suggestion to invoke the minimization tool. This step is now
+performed implicitly if it can be done in a reasonable amount of time (something
+that can be guessed from the number of facts in the original proof and the time
+it took to find it or replay it).
 
 In addition, some provers (notably CVC3, Satallax, and Yices) do not provide
 proofs or sometimes provide incomplete proofs. The minimizer is then invoked to
@@ -667,10 +668,11 @@
 
 where \qty{type\_sys} is a type system specification with the same semantics as
 Sledgehammer's \textit{type\_sys} option (\S\ref{problem-encoding}) and
-\qty{facts} is a list of arbitrary facts. \qty{type\_sys} may also be
-\textit{full\_types}, in which case an appropriate type-sound encoding is
-chosen, \textit{partial\_types} (the default), or \textit{no\_types}, a synonym
-for \textit{erased}.
+\qty{facts} is a list of arbitrary facts. In addition to the values listed in
+\S\ref{problem-encoding}, \qty{type\_sys} may also be \textit{full\_types}, in
+which case an appropriate type-sound encoding is chosen, \textit{partial\_types}
+(the default type-unsound encoding), or \textit{no\_types}, a synonym for
+\textit{erased}.
 
 \section{Option Reference}
 \label{option-reference}