doc-src/Sledgehammer/sledgehammer.tex
changeset 43002 e88fde86e4c2
parent 42996 29be053ec75b
child 43005 c96f06bffd90
equal deleted 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):} \\