doc-src/HOL/logics-HOL.tex

revisiting type annotations for Haskell: necessary type annotations are not inferred on the provided theorems but using the arguments and right hand sides, as these might differ in the case of constants with abstract code types

\documentclass[12pt,a4paper]{report}
\usepackage{../../lib/texinputs/isabelle,../../lib/texinputs/isabellesym}
\usepackage{graphicx,../iman,../extra,../ttbox,../proof,latexsym,../pdfsetup}

%%% to index derived rls:  ^\([a-zA-Z0-9][a-zA-Z0-9_]*\)        \\tdx{\1}  
%%% to index rulenames:   ^ *(\([a-zA-Z0-9][a-zA-Z0-9_]*\),     \\tdx{\1}  
%%% to index constants:   \\tt \([a-zA-Z0-9][a-zA-Z0-9_]*\)     \\cdx{\1}  
%%% to deverbify:         \\verb|\([^|]*\)|     \\ttindex{\1}  


\title{\includegraphics[scale=0.5]{isabelle_hol} \\[4ex]
  Isabelle's Logics: HOL%
  \thanks{The research has been funded by the EPSRC (grants GR/G53279,
    GR\slash H40570, GR/K57381, GR/K77051, GR/M75440), by ESPRIT (projects 3245:
    Logical Frameworks, and 6453: Types) and by the DFG Schwerpunktprogramm
    \emph{Deduktion}.}}

\author{Tobias Nipkow\footnote
{Institut f\"ur Informatik, Technische Universit\"at M\"unchen,
 \texttt{[e-mail]}} and
Lawrence C. Paulson\footnote
{Computer Laboratory, University of Cambridge, \texttt{[e-mail]}} and
Markus Wenzel\footnote
{Institut f\"ur Informatik, Technische Universit\"at M\"unchen,
 \texttt{[e-mail]}}}

\newcommand\subcaption[1]{\par {\centering\normalsize\sc#1\par}\bigskip
  \hrule\bigskip}
\newenvironment{constants}{\begin{center}\small\begin{tabular}{rrrr}}{\end{tabular}\end{center}}

\newcommand\bs{\char '134 }  % A backslash character for \tt font

\makeindex

\underscoreoff

\setcounter{secnumdepth}{2} \setcounter{tocdepth}{2}  %% {secnumdepth}{2}???

\pagestyle{headings}
\sloppy
\binperiod     %%%treat . like a binary operator

\begin{document}
\maketitle 

\begin{abstract}
  This manual describes Isabelle's formalization of Higher-Order Logic, a
  polymorphic version of Church's Simple Theory of Types.  HOL can be best
  understood as a simply-typed version of classical set theory.  The monograph
  \emph{Isabelle/HOL --- A Proof Assistant for Higher-Order Logic} provides a
  gentle introduction on using Isabelle/HOL in practice.
\end{abstract}

\pagenumbering{roman} \tableofcontents \clearfirst
\input{../Logics/syntax}
\include{HOL}
\bibliographystyle{plain}
\bibliography{../manual}
\printindex
\end{document}