| author | paulson |
| Wed, 05 May 1999 16:44:42 +0200 | |
| changeset 6592 | c120262044b6 |
| parent 6588 | 6e6ca099f68f |
| child 6605 | c2754409919b |
| permissions | -rw-r--r-- |
| wenzelm@6580 | 1 |
%% $Id$ |
| wenzelm@6580 | 2 |
\documentclass[12pt]{report}
|
| wenzelm@6580 | 3 |
\usepackage{graphicx,a4,latexsym,../pdfsetup}
|
| wenzelm@6580 | 4 |
|
| wenzelm@6580 | 5 |
\makeatletter |
| wenzelm@6580 | 6 |
\input{../proof.sty}
|
| wenzelm@6580 | 7 |
\input{../rail.sty}
|
| wenzelm@6580 | 8 |
\input{../iman.sty}
|
| wenzelm@6580 | 9 |
\input{../extra.sty}
|
| wenzelm@6580 | 10 |
\makeatother |
| wenzelm@6580 | 11 |
|
| wenzelm@6580 | 12 |
%%% to index derived rls: ^\([a-zA-Z0-9][a-zA-Z0-9_]*\) \\tdx{\1}
|
| wenzelm@6580 | 13 |
%%% to index rulenames: ^ *(\([a-zA-Z0-9][a-zA-Z0-9_]*\), \\tdx{\1}
|
| wenzelm@6580 | 14 |
%%% to index constants: \\tt \([a-zA-Z0-9][a-zA-Z0-9_]*\) \\cdx{\1}
|
| wenzelm@6580 | 15 |
%%% to deverbify: \\verb|\([^|]*\)| \\ttindex{\1}
|
| wenzelm@6580 | 16 |
|
| wenzelm@6580 | 17 |
\title{\includegraphics[scale=0.5]{isabelle_hol.eps} \\[4ex]
|
| wenzelm@6580 | 18 |
Isabelle's Logics: HOL} |
| wenzelm@6580 | 19 |
|
| wenzelm@6580 | 20 |
\author{{\em Lawrence C. Paulson}\\
|
| wenzelm@6580 | 21 |
Computer Laboratory \\ University of Cambridge \\ |
| wenzelm@6580 | 22 |
\texttt{lcp@cl.cam.ac.uk}\\[3ex]
|
| wenzelm@6580 | 23 |
With Contributions by Tobias Nipkow and Markus Wenzel% |
| wenzelm@6580 | 24 |
\thanks{Tobias Nipkow developed~\HOL{}. Markus Wenzel made numerous
|
| wenzelm@6580 | 25 |
improvements. The research has been funded by the EPSRC (grants |
| wenzelm@6580 | 26 |
GR/G53279, GR/H40570, GR/K57381, GR/K77051) and by ESPRIT project |
| wenzelm@6580 | 27 |
6453: Types.}} |
| wenzelm@6580 | 28 |
|
| wenzelm@6580 | 29 |
\newcommand\subcaption[1]{\par {\centering\normalsize\sc#1\par}\bigskip
|
| wenzelm@6580 | 30 |
\hrule\bigskip} |
| wenzelm@6580 | 31 |
\newenvironment{constants}{\begin{center}\small\begin{tabular}{rrrr}}{\end{tabular}\end{center}}
|
| wenzelm@6580 | 32 |
|
| wenzelm@6580 | 33 |
\makeindex |
| wenzelm@6580 | 34 |
|
| wenzelm@6580 | 35 |
\underscoreoff |
| wenzelm@6580 | 36 |
|
| wenzelm@6580 | 37 |
\setcounter{secnumdepth}{2} \setcounter{tocdepth}{2} %% {secnumdepth}{2}???
|
| wenzelm@6580 | 38 |
|
| wenzelm@6580 | 39 |
\pagestyle{headings}
|
| wenzelm@6580 | 40 |
\sloppy |
| wenzelm@6580 | 41 |
\binperiod %%%treat . like a binary operator |
| wenzelm@6580 | 42 |
|
| wenzelm@6580 | 43 |
\begin{document}
|
| wenzelm@6580 | 44 |
\maketitle |
| wenzelm@6580 | 45 |
|
| wenzelm@6580 | 46 |
\begin{abstract}
|
| wenzelm@6580 | 47 |
This manual describes Isabelle's formalization of Higher-Order Logic, a |
| wenzelm@6580 | 48 |
polymorphic version of Church's Simple Theory of Types. HOL can be best |
| wenzelm@6580 | 49 |
understood as a simply-typed version of classical set theory. See also |
| wenzelm@6580 | 50 |
\emph{Isabelle/HOL --- The Tutorial} for a gentle introduction on using
|
| wenzelm@6580 | 51 |
Isabelle/HOL, and the \emph{Isabelle Reference Manual} for general Isabelle
|
| wenzelm@6580 | 52 |
commands. |
| wenzelm@6580 | 53 |
\end{abstract}
|
| wenzelm@6580 | 54 |
|
| wenzelm@6580 | 55 |
\pagenumbering{roman} \tableofcontents \clearfirst
|
| wenzelm@6580 | 56 |
\include{../Logics/syntax}
|
| wenzelm@6580 | 57 |
\include{HOL}
|
| wenzelm@6580 | 58 |
\bibliographystyle{plain}
|
| paulson@6592 | 59 |
\bibliography{../manual}
|
| wenzelm@6580 | 60 |
\input{logics-HOL.ind}
|
| wenzelm@6580 | 61 |
\end{document}
|