minor edits in docs
Thu, 19 Jan 2012 21:37:12 +0100
changeset 46302 adf10579fe43
parent 46301 e2e52c7d25c9
child 46303 0bacd41ce248
minor edits in docs
--- a/doc-src/Sledgehammer/sledgehammer.tex	Thu Jan 19 21:37:12 2012 +0100
+++ b/doc-src/Sledgehammer/sledgehammer.tex	Thu Jan 19 21:37:12 2012 +0100
@@ -1006,9 +1006,9 @@
 are unsound, meaning that they can give rise to spurious proofs
 (unreconstructible using \textit{metis}). The supported type encodings are
 listed below, with an indication of their soundness in parentheses.
-An asterisk (*) indicates that the encodings sometimes lead to reconstruction
-failures in \textit{metis}, unless the \emph{strict} option (described below) is
+An asterisk (*) means that the encoding is slightly incomplete for
+reconstruction with \textit{metis}, unless the \emph{strict} option (described
+below) is enabled.
 \item[\labelitemi] \textbf{\textit{erased} (very unsound):} No type information is
@@ -1132,9 +1132,9 @@
 {\small See also \textit{max\_new\_mono\_instances} (\S\ref{relevance-filter})
 and \textit{max\_mono\_iters} (\S\ref{relevance-filter}).}
 Specifies whether Sledgehammer should run in its strict mode. In that mode,
-sound type encodings marked with an asterisk (*) above are made more reliable
+sound type encodings marked with an asterisk (*) above are made complete
 for reconstruction with \textit{metis}, at the cost of some clutter in the
 generated problems. This option has no effect if \textit{type\_enc} is
 deliberately set to an unsound encoding.