--- a/doc-src/Sledgehammer/sledgehammer.tex Sat Feb 04 07:40:02 2012 +0100
+++ b/doc-src/Sledgehammer/sledgehammer.tex Sat Feb 04 12:08:18 2012 +0100
@@ -722,6 +722,7 @@
\def\optrue#1#2{\flushitem{\textit{#1} $\bigl[$= \qtybf{bool}$\bigr]$\enskip \defl\textit{true}\defr\hfill (neg.: \textit{#2})}\nopagebreak\\[\parskip]}
\def\opfalse#1#2{\flushitem{\textit{#1} $\bigl[$= \qtybf{bool}$\bigr]$\enskip \defl\textit{false}\defr\hfill (neg.: \textit{#2})}\nopagebreak\\[\parskip]}
\def\opsmart#1#2{\flushitem{\textit{#1} $\bigl[$= \qtybf{smart\_bool}$\bigr]$\enskip \defl\textit{smart}\defr\hfill (neg.: \textit{#2})}\nopagebreak\\[\parskip]}
+\def\opsmartx#1#2{\flushitem{\textit{#1} $\bigl[$= \qtybf{smart\_bool}$\bigr]$\enskip \defl\textit{smart}\defr\\\hbox{}\hfill (neg.: \textit{#2})}\nopagebreak\\[\parskip]}
\def\opnodefault#1#2{\flushitem{\textit{#1} = \qtybf{#2}} \nopagebreak\\[\parskip]}
\def\opnodefaultbrk#1#2{\flushitem{$\bigl[$\textit{#1} =$\bigr]$ \qtybf{#2}} \nopagebreak\\[\parskip]}
\def\opdefault#1#2#3{\flushitem{\textit{#1} = \qtybf{#2}\enskip \defl\textit{#3}\defr} \nopagebreak\\[\parskip]}
@@ -1005,6 +1006,10 @@
For SMT solvers, the $\lambda$ translation scheme is always \textit{lifting},
irrespective of the value of this option.
+\opsmartx{uncurried\_aliases}{no\_uncurried\_aliases}
+Specifies the $\lambda$ translation scheme to use in ATP problems. The supported
+translation schemes are listed below:
+
\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