# HG changeset patch
# User blanchet
# Date 1309528418 -7200
# Node ID ecd4bb7a8bc0f5f1f1285b66776cb78ba880cf3b
# Parent  a867ebb122090121741bfebe35160eea59fd5bdb
update documentation after "type_enc" renaming + fixed a few other out-of-date factlets

diff -r a867ebb12209 -r ecd4bb7a8bc0 NEWS
--- a/NEWS	Fri Jul 01 15:53:38 2011 +0200
+++ b/NEWS	Fri Jul 01 15:53:38 2011 +0200
@@ -81,14 +81,14 @@
     INCOMPATIBILITY.
 
 * Sledgehammer:
-  - sledgehammer available_provers ~> sledgehammer supported_provers
+  - sledgehammer available_provers ~> sledgehammer supported_provers.
     INCOMPATIBILITY.
   - Added support for SNARK and ToFoF-E on SystemOnTPTP and for simply typed
     TPTP problems (TFF).
-  - Added "type_sys", "sound", "max_mono_iters", and "max_new_mono_instances"
-    options.
-  - Removed "full_types" option and corresponding Proof General menu item.
-    INCOMPATIBILITY.
+  - Added "preplay_timeout", "slicing", "type_enc", "sound", "max_mono_iters",
+    and "max_new_mono_instances" options.
+  - Removed "explicit_apply" and "full_types" options as well as "Full Types"
+    Proof General menu item. INCOMPATIBILITY.
 
 * Metis:
   - Removed "metisF" -- use "metis" instead. INCOMPATIBILITY.
diff -r a867ebb12209 -r ecd4bb7a8bc0 doc-src/Sledgehammer/sledgehammer.tex
--- a/doc-src/Sledgehammer/sledgehammer.tex	Fri Jul 01 15:53:38 2011 +0200
+++ b/doc-src/Sledgehammer/sledgehammer.tex	Fri Jul 01 15:53:38 2011 +0200
@@ -177,14 +177,14 @@
 set the environment variable \texttt{E\_HOME}, \texttt{SPASS\_HOME}, or
 \texttt{VAMPIRE\_HOME} to the directory that contains the \texttt{eproof},
 \texttt{SPASS}, or \texttt{vampire} executable. Sledgehammer has been tested
-with E 1.0 and 1.2, SPASS 3.5 and 3.7, and Vampire 0.6 and 1.0%
+with E 1.0 to 1.3, SPASS 3.5 and 3.7, and Vampire 0.6 and 1.0%
 \footnote{Following the rewrite of Vampire, the counter for version numbers was
 reset to 0; hence the (new) Vampire versions 0.6 and 1.0 are more recent than,
 say, Vampire 11.5.}%
 . Since the ATPs' output formats are neither documented nor stable, other
 versions of the ATPs might or might not work well with Sledgehammer. Ideally,
 also set \texttt{E\_VERSION}, \texttt{SPASS\_VERSION}, or
-\texttt{VAMPIRE\_VERSION} to the ATP's version number (e.g., ``1.2'').
+\texttt{VAMPIRE\_VERSION} to the ATP's version number (e.g., ``1.3'').
 \end{enum}
 
 To check whether E and SPASS are successfully installed, follow the example in
@@ -401,7 +401,7 @@
 This message usually indicates that Sledgehammer found a type-incorrect proof.
 This was a frequent issue with older versions of Sledgehammer, which did not
 supply enough typing information to the ATPs by default. If you notice many
-unsound proofs and are not using \textit{type\_sys} (\S\ref{problem-encoding}),
+unsound proofs and are not using \textit{type\_enc} (\S\ref{problem-encoding}),
 contact the author at \authoremail.
 
 \point{How can I tell whether a generated proof is sound?}
@@ -646,13 +646,13 @@
 The \textit{metis} proof method has the syntax
 
 \prew
-\textbf{\textit{metis}}~(\qty{type\_sys})${}^?$~\qty{facts}${}^?$
+\textbf{\textit{metis}}~(\qty{type\_enc})${}^?$~\qty{facts}${}^?$
 \postw
 
-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
+where \qty{type\_enc} is a type encoding specification with the same semantics
+as Sledgehammer's \textit{type\_enc} option (\S\ref{problem-encoding}) and
 \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
+\S\ref{problem-encoding}, \qty{type\_enc} 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}.
@@ -876,11 +876,11 @@
 \label{problem-encoding}
 
 \begin{enum}
-\opdefault{type\_sys}{string}{smart}
-Specifies the type system to use in ATP problems. Some of the type systems are
-unsound, meaning that they can give rise to spurious proofs (unreconstructible
-using Metis). The supported type systems are listed below, with an indication of
-their soundness in parentheses:
+\opdefault{type\_enc}{string}{smart}
+Specifies the type encoding to use in ATP problems. Some of the type encodings
+are unsound, meaning that they can give rise to spurious proofs
+(unreconstructible using Metis). The supported type encodings are listed below,
+with an indication of their soundness in parentheses:
 
 \begin{enum}
 \item[$\bullet$] \textbf{\textit{erased} (very unsound):} No type information is
@@ -935,7 +935,7 @@
 \textbf{%
 \textit{poly\_preds}?, \textit{poly\_tags}?, \textit{mono\_preds}?, \textit{mono\_tags}?, \\
 \textit{mangled\_preds}?, \textit{mangled\_tags}?, \textit{simple}?, \textit{simple\_higher}? (quasi-sound):} \\
-The type systems \textit{poly\_preds}, \textit{poly\_tags},
+The type encodings \textit{poly\_preds}, \textit{poly\_tags},
 \textit{mono\_preds}, \textit{mono\_tags}, \textit{mangled\_preds},
 \textit{mangled\_tags}, \textit{simple}, and \textit{simple\_higher} are fully
 typed and sound. For each of these, Sledgehammer also provides a lighter,
@@ -951,7 +951,7 @@
 \textit{poly\_preds}!, \textit{poly\_tags}!, \textit{mono\_preds}!, \textit{mono\_tags}!, \\
 \textit{mangled\_preds}!, \textit{mangled\_tags}!, \textit{simple}!, \textit{simple\_higher}! \\
 (mildly unsound):} \\
-The type systems \textit{poly\_preds}, \textit{poly\_tags},
+The type encodings \textit{poly\_preds}, \textit{poly\_tags},
 \textit{mono\_preds}, \textit{mono\_tags}, \textit{mangled\_preds},
 \textit{mangled\_tags}, \textit{simple}, and \textit{simple\_higher} also admit
 a mildly unsound (but very efficient) variant identified by an exclamation mark
@@ -965,14 +965,14 @@
 the ATP and should be the most efficient virtually sound encoding for that ATP.
 \end{enum}
 
-In addition, all the \textit{preds} and \textit{tags} type systems are available
-in two variants, a lightweight and a heavyweight variant. The lightweight
-variants are generally more efficient and are the default; the heavyweight
-variants are identified by a \textit{\_heavy} suffix (e.g.,
+In addition, all the \textit{preds} and \textit{tags} type encodings are
+available in two variants, a lightweight and a heavyweight variant. The
+lightweight variants are generally more efficient and are the default; the
+heavyweight variants are identified by a \textit{\_heavy} suffix (e.g.,
 \textit{mangled\_preds\_heavy}{?}).
 
-For SMT solvers, the type system is always \textit{simple}, irrespective of the
-value of this option.
+For SMT solvers, the type encoding is always \textit{simple}, irrespective of
+the value of this option.
 
 \nopagebreak
 {\small See also \textit{max\_new\_mono\_instances} (\S\ref{relevance-filter})
@@ -1006,19 +1006,19 @@
 Specifies the maximum number of monomorphic instances to generate beyond
 \textit{max\_relevant}. The higher this limit is, the more monomorphic instances
 are potentially generated. Whether monomorphization takes place depends on the
-type system used.
+type encoding used.
 
 \nopagebreak
-{\small See also \textit{type\_sys} (\S\ref{problem-encoding}).}
+{\small See also \textit{type\_enc} (\S\ref{problem-encoding}).}
 
 \opdefault{max\_mono\_iters}{int}{\upshape 3}
 Specifies the maximum number of iterations for the monomorphization fixpoint
 construction. The higher this limit is, the more monomorphic instances are
 potentially generated. Whether monomorphization takes place depends on the
-type system used.
+type encoding used.
 
 \nopagebreak
-{\small See also \textit{type\_sys} (\S\ref{problem-encoding}).}
+{\small See also \textit{type\_enc} (\S\ref{problem-encoding}).}
 \end{enum}
 
 \subsection{Output Format}