# HG changeset patch
# User blanchet
# Date 1306485007 -7200
# Node ID e88fde86e4c23b3a78df64f5ff733770e9ba2cbc
# Parent  f3492698dfc752e82d799f370cbb149d20a7b6c4
mention contributions from LCP and explain metis and metisFT encodings

diff -r f3492698dfc7 -r e88fde86e4c2 doc-src/Sledgehammer/sledgehammer.tex
--- a/doc-src/Sledgehammer/sledgehammer.tex	Fri May 27 10:30:07 2011 +0200
+++ b/doc-src/Sledgehammer/sledgehammer.tex	Fri May 27 10:30:07 2011 +0200
@@ -44,7 +44,10 @@
 \Large A User's Guide to Sledgehammer for Isabelle/HOL}
 \author{\hbox{} \\
 Jasmin Christian Blanchette \\
-{\normalsize Institut f\"ur Informatik, Technische Universit\"at M\"unchen} \\
+{\normalsize Institut f\"ur Informatik, Technische Universit\"at M\"unchen} \\[4\smallskipamount]
+{\normalsize with contributions from} \\[4\smallskipamount]
+Lawrence C. Paulson \\
+{\normalsize Computer Laboratory, University of Cambridge} \\
 \hbox{}}
 
 \maketitle
@@ -884,11 +887,14 @@
 arguments, to resolve overloading.
 
 \item[$\bullet$] \textbf{\textit{poly\_tags} (sound):} Each term and subterm is
-tagged with its type using a function $\mathit{type\_info\/}(\tau, t)$.
+tagged with its type using a function $\mathit{type\_info\/}(\tau, t)$. This
+coincides with the encoding used by the \textit{metisFT} command.
 
 \item[$\bullet$] \textbf{\textit{poly\_args} (unsound):}
 Like for \textit{poly\_preds} constants are annotated with their types to
-resolve overloading, but otherwise no type information is encoded.
+resolve overloading, but otherwise no type information is encoded. This
+coincides with the encoding used by the \textit{metis} command (before it falls
+back on \textit{metisFT}).
 
 \item[$\bullet$]
 \textbf{%