--- a/doc-src/Sledgehammer/sledgehammer.tex Wed May 04 22:56:33 2011 +0200
+++ b/doc-src/Sledgehammer/sledgehammer.tex Wed May 04 23:18:28 2011 +0200
@@ -583,10 +583,14 @@
Constants are annotated with their types, supplied as extra arguments, to
resolve overloading.
+\item[$\bullet$] \textbf{\textit{tags}:} Each term and subterm is tagged with
+its type using a function $\mathit{type\_info\/}(\tau, t)$.
+
\item[$\bullet$] \textbf{\textit{mono\_preds}:} Similar to \textit{preds}, but
-the problem is additionally monomorphized. This corresponds to the traditional
-encoding of types in an untyped logic without overloading (e.g., such as
-performed by the ToFoF-E wrapper).
+the problem is additionally monomorphized.
+
+\item[$\bullet$] \textbf{\textit{mono\_tags}:} Similar to \textit{tags}, but
+the problem is additionally monomorphized.
\item[$\bullet$] \textbf{\textit{mangled\_preds}:} Similar to
\textit{mono\_preds}, but types are mangled in constant names instead of being
@@ -594,12 +598,6 @@
$\mathit{has\_type\/}(\tau, t)$ becomes a unary predicate
$\mathit{has\_type\_}\tau(t)$.
-\item[$\bullet$] \textbf{\textit{tags}:} Each term and subterm is tagged with
-its type using a function $\mathit{type\_info\/}(\tau, t)$.
-
-\item[$\bullet$] \textbf{\textit{mono\_tags}:} Similar to \textit{tags}, but
-the problem is additionally monomorphized.
-
\item[$\bullet$] \textbf{\textit{mangled\_tags}:} Similar to
\textit{mono\_tags}, but types are mangled in constant names instead of being
supplied as ground term arguments. The binary function