doc-src/Sledgehammer/sledgehammer.tex
 changeset 43002 e88fde86e4c2 parent 42996 29be053ec75b child 43005 c96f06bffd90
equal inserted replaced
43001:f3492698dfc7 43002:e88fde86e4c2
    42 \title{\includegraphics[scale=0.5]{isabelle_sledgehammer} \\[4ex]
    42 \title{\includegraphics[scale=0.5]{isabelle_sledgehammer} \\[4ex]
    43 Hammering Away \\[\smallskipamount]
    43 Hammering Away \\[\smallskipamount]
    44 \Large A User's Guide to Sledgehammer for Isabelle/HOL}
    44 \Large A User's Guide to Sledgehammer for Isabelle/HOL}
    45 \author{\hbox{} \\
    45 \author{\hbox{} \\
    46 Jasmin Christian Blanchette \\
    46 Jasmin Christian Blanchette \\
    47 {\normalsize Institut f\"ur Informatik, Technische Universit\"at M\"unchen} \\
    47 {\normalsize Institut f\"ur Informatik, Technische Universit\"at M\"unchen} \\[4\smallskipamount]

    48 {\normalsize with contributions from} \\[4\smallskipamount]

    49 Lawrence C. Paulson \\

    50 {\normalsize Computer Laboratory, University of Cambridge} \\
    48 \hbox{}}
    51 \hbox{}}
    49
    52
    50 \maketitle
    53 \maketitle
    51
    54
    52 \tableofcontents
    55 \tableofcontents
   882 a predicate \textit{has\_\allowbreak type\/}$(\tau, t)$ that restricts the range
   885 a predicate \textit{has\_\allowbreak type\/}$(\tau, t)$ that restricts the range
   883 of bound variables. Constants are annotated with their types, supplied as extra
   886 of bound variables. Constants are annotated with their types, supplied as extra
   884 arguments, to resolve overloading.
   887 arguments, to resolve overloading.
   885
   888
   886 \item[$\bullet$] \textbf{\textit{poly\_tags} (sound):} Each term and subterm is
   889 \item[$\bullet$] \textbf{\textit{poly\_tags} (sound):} Each term and subterm is
   887 tagged with its type using a function $\mathit{type\_info\/}(\tau, t)$.
   890 tagged with its type using a function $\mathit{type\_info\/}(\tau, t)$. This

   891 coincides with the encoding used by the \textit{metisFT} command.
   888
   892
   889 \item[$\bullet$] \textbf{\textit{poly\_args} (unsound):}
   893 \item[$\bullet$] \textbf{\textit{poly\_args} (unsound):}
   890 Like for \textit{poly\_preds} constants are annotated with their types to
   894 Like for \textit{poly\_preds} constants are annotated with their types to
   891 resolve overloading, but otherwise no type information is encoded.
   895 resolve overloading, but otherwise no type information is encoded. This

   896 coincides with the encoding used by the \textit{metis} command (before it falls

   897 back on \textit{metisFT}).
   892
   898
   893 \item[$\bullet$]
   899 \item[$\bullet$]
   894 \textbf{%
   900 \textbf{%
   895 \textit{mono\_preds}, \textit{mono\_tags} (sound);
   901 \textit{mono\_preds}, \textit{mono\_tags} (sound);
   896 \textit{mono\_args} (unsound):} \\
   902 \textit{mono\_args} (unsound):} \\