1.1 --- a/NEWS	Fri Jul 01 15:53:38 2011 +0200
     1.2 +++ b/NEWS	Fri Jul 01 15:53:38 2011 +0200
     1.3 @@ -81,14 +81,14 @@
     1.4      INCOMPATIBILITY.
     1.5  
     1.6  * Sledgehammer:
     1.7 -  - sledgehammer available_provers ~> sledgehammer supported_provers
     1.8 +  - sledgehammer available_provers ~> sledgehammer supported_provers.
     1.9      INCOMPATIBILITY.
    1.10    - Added support for SNARK and ToFoF-E on SystemOnTPTP and for simply typed
    1.11      TPTP problems (TFF).
    1.12 -  - Added "type_sys", "sound", "max_mono_iters", and "max_new_mono_instances"
    1.13 -    options.
    1.14 -  - Removed "full_types" option and corresponding Proof General menu item.
    1.15 -    INCOMPATIBILITY.
    1.16 +  - Added "preplay_timeout", "slicing", "type_enc", "sound", "max_mono_iters",
    1.17 +    and "max_new_mono_instances" options.
    1.18 +  - Removed "explicit_apply" and "full_types" options as well as "Full Types"
    1.19 +    Proof General menu item. INCOMPATIBILITY.
    1.20  
    1.21  * Metis:
    1.22    - Removed "metisF" -- use "metis" instead. INCOMPATIBILITY.

     2.1 --- a/doc-src/Sledgehammer/sledgehammer.tex	Fri Jul 01 15:53:38 2011 +0200
     2.2 +++ b/doc-src/Sledgehammer/sledgehammer.tex	Fri Jul 01 15:53:38 2011 +0200
     2.3 @@ -177,14 +177,14 @@
     2.4  set the environment variable \texttt{E\_HOME}, \texttt{SPASS\_HOME}, or
     2.5  \texttt{VAMPIRE\_HOME} to the directory that contains the \texttt{eproof},
     2.6  \texttt{SPASS}, or \texttt{vampire} executable. Sledgehammer has been tested
     2.7 -with E 1.0 and 1.2, SPASS 3.5 and 3.7, and Vampire 0.6 and 1.0%
     2.8 +with E 1.0 to 1.3, SPASS 3.5 and 3.7, and Vampire 0.6 and 1.0%
     2.9  \footnote{Following the rewrite of Vampire, the counter for version numbers was
    2.10  reset to 0; hence the (new) Vampire versions 0.6 and 1.0 are more recent than,
    2.11  say, Vampire 11.5.}%
    2.12  . Since the ATPs' output formats are neither documented nor stable, other
    2.13  versions of the ATPs might or might not work well with Sledgehammer. Ideally,
    2.14  also set \texttt{E\_VERSION}, \texttt{SPASS\_VERSION}, or
    2.15 -\texttt{VAMPIRE\_VERSION} to the ATP's version number (e.g., ``1.2'').
    2.16 +\texttt{VAMPIRE\_VERSION} to the ATP's version number (e.g., ``1.3'').
    2.17  \end{enum}
    2.18  
    2.19  To check whether E and SPASS are successfully installed, follow the example in
    2.20 @@ -401,7 +401,7 @@
    2.21  This message usually indicates that Sledgehammer found a type-incorrect proof.
    2.22  This was a frequent issue with older versions of Sledgehammer, which did not
    2.23  supply enough typing information to the ATPs by default. If you notice many
    2.24 -unsound proofs and are not using \textit{type\_sys} (\S\ref{problem-encoding}),
    2.25 +unsound proofs and are not using \textit{type\_enc} (\S\ref{problem-encoding}),
    2.26  contact the author at \authoremail.
    2.27  
    2.28  \point{How can I tell whether a generated proof is sound?}
    2.29 @@ -646,13 +646,13 @@
    2.30  The \textit{metis} proof method has the syntax
    2.31  
    2.32  \prew
    2.33 -\textbf{\textit{metis}}~(\qty{type\_sys})${}^?$~\qty{facts}${}^?$
    2.34 +\textbf{\textit{metis}}~(\qty{type\_enc})${}^?$~\qty{facts}${}^?$
    2.35  \postw
    2.36  
    2.37 -where \qty{type\_sys} is a type system specification with the same semantics as
    2.38 -Sledgehammer's \textit{type\_sys} option (\S\ref{problem-encoding}) and
    2.39 +where \qty{type\_enc} is a type encoding specification with the same semantics
    2.40 +as Sledgehammer's \textit{type\_enc} option (\S\ref{problem-encoding}) and
    2.41  \qty{facts} is a list of arbitrary facts. In addition to the values listed in
    2.42 -\S\ref{problem-encoding}, \qty{type\_sys} may also be \textit{full\_types}, in
    2.43 +\S\ref{problem-encoding}, \qty{type\_enc} may also be \textit{full\_types}, in
    2.44  which case an appropriate type-sound encoding is chosen, \textit{partial\_types}
    2.45  (the default type-unsound encoding), or \textit{no\_types}, a synonym for
    2.46  \textit{erased}.
    2.47 @@ -876,11 +876,11 @@
    2.48  \label{problem-encoding}
    2.49  
    2.50  \begin{enum}
    2.51 -\opdefault{type\_sys}{string}{smart}
    2.52 -Specifies the type system to use in ATP problems. Some of the type systems are
    2.53 -unsound, meaning that they can give rise to spurious proofs (unreconstructible
    2.54 -using Metis). The supported type systems are listed below, with an indication of
    2.55 -their soundness in parentheses:
    2.56 +\opdefault{type\_enc}{string}{smart}
    2.57 +Specifies the type encoding to use in ATP problems. Some of the type encodings
    2.58 +are unsound, meaning that they can give rise to spurious proofs
    2.59 +(unreconstructible using Metis). The supported type encodings are listed below,
    2.60 +with an indication of their soundness in parentheses:
    2.61  
    2.62  \begin{enum}
    2.63  \item[$\bullet$] \textbf{\textit{erased} (very unsound):} No type information is
    2.64 @@ -935,7 +935,7 @@
    2.65  \textbf{%
    2.66  \textit{poly\_preds}?, \textit{poly\_tags}?, \textit{mono\_preds}?, \textit{mono\_tags}?, \\
    2.67  \textit{mangled\_preds}?, \textit{mangled\_tags}?, \textit{simple}?, \textit{simple\_higher}? (quasi-sound):} \\
    2.68 -The type systems \textit{poly\_preds}, \textit{poly\_tags},
    2.69 +The type encodings \textit{poly\_preds}, \textit{poly\_tags},
    2.70  \textit{mono\_preds}, \textit{mono\_tags}, \textit{mangled\_preds},
    2.71  \textit{mangled\_tags}, \textit{simple}, and \textit{simple\_higher} are fully
    2.72  typed and sound. For each of these, Sledgehammer also provides a lighter,
    2.73 @@ -951,7 +951,7 @@
    2.74  \textit{poly\_preds}!, \textit{poly\_tags}!, \textit{mono\_preds}!, \textit{mono\_tags}!, \\
    2.75  \textit{mangled\_preds}!, \textit{mangled\_tags}!, \textit{simple}!, \textit{simple\_higher}! \\
    2.76  (mildly unsound):} \\
    2.77 -The type systems \textit{poly\_preds}, \textit{poly\_tags},
    2.78 +The type encodings \textit{poly\_preds}, \textit{poly\_tags},
    2.79  \textit{mono\_preds}, \textit{mono\_tags}, \textit{mangled\_preds},
    2.80  \textit{mangled\_tags}, \textit{simple}, and \textit{simple\_higher} also admit
    2.81  a mildly unsound (but very efficient) variant identified by an exclamation mark
    2.82 @@ -965,14 +965,14 @@
    2.83  the ATP and should be the most efficient virtually sound encoding for that ATP.
    2.84  \end{enum}
    2.85  
    2.86 -In addition, all the \textit{preds} and \textit{tags} type systems are available
    2.87 -in two variants, a lightweight and a heavyweight variant. The lightweight
    2.88 -variants are generally more efficient and are the default; the heavyweight
    2.89 -variants are identified by a \textit{\_heavy} suffix (e.g.,
    2.90 +In addition, all the \textit{preds} and \textit{tags} type encodings are
    2.91 +available in two variants, a lightweight and a heavyweight variant. The
    2.92 +lightweight variants are generally more efficient and are the default; the
    2.93 +heavyweight variants are identified by a \textit{\_heavy} suffix (e.g.,
    2.94  \textit{mangled\_preds\_heavy}{?}).
    2.95  
    2.96 -For SMT solvers, the type system is always \textit{simple}, irrespective of the
    2.97 -value of this option.
    2.98 +For SMT solvers, the type encoding is always \textit{simple}, irrespective of
    2.99 +the value of this option.
   2.100  
   2.101  \nopagebreak
   2.102  {\small See also \textit{max\_new\_mono\_instances} (\S\ref{relevance-filter})
   2.103 @@ -1006,19 +1006,19 @@
   2.104  Specifies the maximum number of monomorphic instances to generate beyond
   2.105  \textit{max\_relevant}. The higher this limit is, the more monomorphic instances
   2.106  are potentially generated. Whether monomorphization takes place depends on the
   2.107 -type system used.
   2.108 +type encoding used.
   2.109  
   2.110  \nopagebreak
   2.111 -{\small See also \textit{type\_sys} (\S\ref{problem-encoding}).}
   2.112 +{\small See also \textit{type\_enc} (\S\ref{problem-encoding}).}
   2.113  
   2.114  \opdefault{max\_mono\_iters}{int}{\upshape 3}
   2.115  Specifies the maximum number of iterations for the monomorphization fixpoint
   2.116  construction. The higher this limit is, the more monomorphic instances are
   2.117  potentially generated. Whether monomorphization takes place depends on the
   2.118 -type system used.
   2.119 +type encoding used.
   2.120  
   2.121  \nopagebreak
   2.122 -{\small See also \textit{type\_sys} (\S\ref{problem-encoding}).}
   2.123 +{\small See also \textit{type\_enc} (\S\ref{problem-encoding}).}
   2.124  \end{enum}
   2.125  
   2.126  \subsection{Output Format}