wenzelm@6580: %% $Id$
wenzelm@6580: \documentclass[12pt]{report}
wenzelm@6580: \usepackage{graphicx,a4,latexsym,../pdfsetup}
wenzelm@6580: 
wenzelm@6580: \makeatletter
wenzelm@6580: \input{../proof.sty}
wenzelm@6580: \input{../rail.sty}
wenzelm@6580: \input{../iman.sty}
wenzelm@6580: \input{../extra.sty}
wenzelm@6580: \makeatother
wenzelm@6580: 
wenzelm@6580: %%% to index derived rls:  ^\([a-zA-Z0-9][a-zA-Z0-9_]*\)        \\tdx{\1}  
wenzelm@6580: %%% to index rulenames:   ^ *(\([a-zA-Z0-9][a-zA-Z0-9_]*\),     \\tdx{\1}  
wenzelm@6580: %%% to index constants:   \\tt \([a-zA-Z0-9][a-zA-Z0-9_]*\)     \\cdx{\1}  
wenzelm@6580: %%% to deverbify:         \\verb|\([^|]*\)|     \\ttindex{\1}  
wenzelm@6580: 
wenzelm@6580: \title{\includegraphics[scale=0.5]{isabelle_hol.eps} \\[4ex] 
wenzelm@6580:        Isabelle's Logics: HOL}
wenzelm@6580: 
wenzelm@6580: \author{{\em Lawrence C. Paulson}\\
wenzelm@6580:         Computer Laboratory \\ University of Cambridge \\
wenzelm@6580:         \texttt{lcp@cl.cam.ac.uk}\\[3ex] 
wenzelm@6580:         With Contributions by Tobias Nipkow and Markus Wenzel%
wenzelm@6580:         \thanks{Tobias Nipkow developed~\HOL{}.  Markus Wenzel made numerous
wenzelm@6580:           improvements.  The research has been funded by the EPSRC (grants
wenzelm@6580:           GR/G53279, GR/H40570, GR/K57381, GR/K77051) and by ESPRIT project
wenzelm@6580:           6453: Types.}}
wenzelm@6580: 
wenzelm@6580: \newcommand\subcaption[1]{\par {\centering\normalsize\sc#1\par}\bigskip
wenzelm@6580:   \hrule\bigskip}
wenzelm@6580: \newenvironment{constants}{\begin{center}\small\begin{tabular}{rrrr}}{\end{tabular}\end{center}}
wenzelm@6580: 
wenzelm@6580: \makeindex
wenzelm@6580: 
wenzelm@6580: \underscoreoff
wenzelm@6580: 
wenzelm@6580: \setcounter{secnumdepth}{2} \setcounter{tocdepth}{2}  %% {secnumdepth}{2}???
wenzelm@6580: 
wenzelm@6580: \pagestyle{headings}
wenzelm@6580: \sloppy
wenzelm@6580: \binperiod     %%%treat . like a binary operator
wenzelm@6580: 
wenzelm@6580: \begin{document}
wenzelm@6580: \maketitle 
wenzelm@6580: 
wenzelm@6580: \begin{abstract}
wenzelm@6580:   This manual describes Isabelle's formalization of Higher-Order Logic, a
wenzelm@6580:   polymorphic version of Church's Simple Theory of Types.  HOL can be best
wenzelm@6580:   understood as a simply-typed version of classical set theory.  See also
wenzelm@6580:   \emph{Isabelle/HOL --- The Tutorial} for a gentle introduction on using
wenzelm@6580:   Isabelle/HOL, and the \emph{Isabelle Reference Manual} for general Isabelle
wenzelm@6580:   commands.
wenzelm@6580: \end{abstract}
wenzelm@6580: 
wenzelm@6580: \pagenumbering{roman} \tableofcontents \clearfirst
wenzelm@6580: \include{../Logics/syntax}
wenzelm@6580: \include{HOL}
wenzelm@6580: \bibliographystyle{plain}
paulson@6592: \bibliography{../manual}
wenzelm@6580: \input{logics-HOL.ind}
wenzelm@6580: \end{document}