1.1 --- a/NEWS	Mon Apr 04 18:53:35 2011 +0200
     1.2 +++ b/NEWS	Mon Apr 04 19:09:10 2011 +0200
     1.3 @@ -49,7 +49,7 @@
     1.4  * Sledgehammer:
     1.5    - sledgehammer available_provers ~> sledgehammer supported_provers
     1.6      INCOMPATIBILITY.
     1.7 -  - Added "monomorphize" and "monomorphize_limit" options.
     1.8 +  - Added "monomorphize", "monomorphize_limit", and "type_sys" options.
     1.9  
    1.10  * "try":
    1.11    - Added "simp:", "intro:", and "elim:" options.

     2.1 --- a/doc-src/Sledgehammer/sledgehammer.tex	Mon Apr 04 18:53:35 2011 +0200
     2.2 +++ b/doc-src/Sledgehammer/sledgehammer.tex	Mon Apr 04 19:09:10 2011 +0200
     2.3 @@ -476,7 +476,7 @@
     2.4  \end{enum}
     2.5  
     2.6  By default, Sledgehammer will run E, SPASS, Vampire, SInE-E, and Z3 (or whatever
     2.7 -the SMT module's \emph{smt\_solver} configuration option is set to) in
     2.8 +the SMT module's \textit{smt\_solver} configuration option is set to) in
     2.9  parallel---either locally or remotely, depending on the number of processor
    2.10  cores available. For historical reasons, the default value of this option can be
    2.11  overridden using the option ``Sledgehammer: Provers'' from the ``Isabelle'' menu
    2.12 @@ -536,6 +536,55 @@
    2.13  tends to slow down the ATPs significantly. For historical reasons, the default
    2.14  value of this option can be overridden using the option ``Sledgehammer: Full
    2.15  Types'' from the ``Isabelle'' menu in Proof General.
    2.16 +
    2.17 +\opfalse{full\_types}{partial\_types}
    2.18 +Specifies whether full-type information is encoded in ATP problems. Enabling
    2.19 +this option can prevent the discovery of type-incorrect proofs, but it also
    2.20 +tends to slow down the ATPs significantly. For historical reasons, the default
    2.21 +value of this option can be overridden using the option ``Sledgehammer: Full
    2.22 +Types'' from the ``Isabelle'' menu in Proof General.
    2.23 +
    2.24 +\opfalse{monomorphize}{dont\_monomorphize}
    2.25 +Specifies whether the relevant facts should be monomorphized---i.e., whether
    2.26 +their type variables should be instantiated with relevant ground types.
    2.27 +Monomorphization is always performed for SMT solvers, irrespective of this
    2.28 +option. Monomorphization can simplify reasoning but also leads to larger fact
    2.29 +bases, which can slow down the ATPs.
    2.30 +
    2.31 +\opdefault{monomorphize\_limit}{int}{\upshape 4}
    2.32 +Specifies the maximum number of iterations for the monomorphization fixpoint
    2.33 +construction. The higher this limit is, the more monomorphic instances are
    2.34 +potentially generated.
    2.35 +
    2.36 +\opdefault{type\_sys}{string}{smart}
    2.37 +Specifies the type system to use in ATP problems. The option can take the
    2.38 +following values:
    2.39 +
    2.40 +\begin{enum}
    2.41 +\item[$\bullet$] \textbf{\textit{tags}:} Each term (and subterm) is tagged with
    2.42 +its type.
    2.43 +
    2.44 +% NOT YET IMPLEMENTED:
    2.45 +%\item[$\bullet$] \textbf{\textit{preds}:} Types are represented by predicates.
    2.46 +
    2.47 +\item[$\bullet$] \textbf{\textit{mangled}:} Types are mangled in constant names.
    2.48 +This value is available only if \textit{monomorphize} is enabled and
    2.49 +\textit{full\_types} is enabled.
    2.50 +
    2.51 +\item[$\bullet$] \textbf{\textit{const\_args}:} Constants are annotated with
    2.52 +their type parameters, which are passed as extra arguments. This value is not
    2.53 +available if \textit{full\_types} is enabled.
    2.54 +
    2.55 +\item[$\bullet$] \textbf{\textit{none}:} No type information is supplied to the
    2.56 +ATP.
    2.57 +
    2.58 +\item[$\bullet$] \textbf{\textit{smart}:} This is the same as
    2.59 +\textit{tags} if \textit{full\_types} is enabled; otherwise, this is the
    2.60 +same as \textit{mangled} if \textit{monomorphize} is enabled and
    2.61 +\textit{const\_args} otherwise.
    2.62 +\end{enum}
    2.63 +
    2.64 +For SMT solvers, the type system is always \textit{mangled}.
    2.65  \end{enum}
    2.66  
    2.67  \subsection{Relevance Filter}
    2.68 @@ -556,18 +605,6 @@
    2.69  empirically found to be appropriate for the prover. A typical value would be
    2.70  300.
    2.71  
    2.72 -\opfalse{monomorphize}{dont\_monomorphize}
    2.73 -Specifies whether the relevant facts should be monomorphized---i.e., whether
    2.74 -their type variables should be instantiated with relevant ground types.
    2.75 -Monomorphization is always performed for SMT solvers, irrespective of this
    2.76 -option. Monomorphization can simplify reasoning but also leads to larger fact
    2.77 -bases, which can slow down the ATPs.
    2.78 -
    2.79 -\opdefault{monomorphize\_limit}{int}{\upshape 4}
    2.80 -Specifies the maximum number of iterations for the monomorphization fixpoint
    2.81 -construction. The higher this limit is, the more monomorphic instances are
    2.82 -potentially generated.
    2.83 -
    2.84  \end{enum}
    2.85  
    2.86  \subsection{Output Format}