|
1 %% $Id$ |
|
2 \documentclass[12pt]{report} |
|
3 \usepackage{graphicx,a4,latexsym,../pdfsetup} |
|
4 |
|
5 \makeatletter |
|
6 \input{../proof.sty} |
|
7 \input{../rail.sty} |
|
8 \input{../iman.sty} |
|
9 \input{../extra.sty} |
|
10 \makeatother |
|
11 |
|
12 %%% to index derived rls: ^\([a-zA-Z0-9][a-zA-Z0-9_]*\) \\tdx{\1} |
|
13 %%% to index rulenames: ^ *(\([a-zA-Z0-9][a-zA-Z0-9_]*\), \\tdx{\1} |
|
14 %%% to index constants: \\tt \([a-zA-Z0-9][a-zA-Z0-9_]*\) \\cdx{\1} |
|
15 %%% to deverbify: \\verb|\([^|]*\)| \\ttindex{\1} |
|
16 |
|
17 \title{\includegraphics[scale=0.5]{isabelle.eps} \\[4ex] |
|
18 Isabelle's Logics: FOL and ZF} |
|
19 |
|
20 \author{{\em Lawrence C. Paulson}\\ |
|
21 Computer Laboratory \\ University of Cambridge \\ |
|
22 \texttt{lcp@cl.cam.ac.uk}\\[3ex] |
|
23 With Contributions by Tobias Nipkow and Markus Wenzel% |
|
24 \thanks{Markus Wenzel made numerous improvements. |
|
25 Philippe de Groote and contributed to~\ZF{}. Philippe No\"el and |
|
26 Martin Coen made many contributions to~\ZF{}. The research has |
|
27 been funded by the EPSRC (grants GR/G53279, GR/H40570, GR/K57381, |
|
28 GR/K77051) and by ESPRIT project 6453: Types.} |
|
29 } |
|
30 |
|
31 \newcommand\subcaption[1]{\par {\centering\normalsize\sc#1\par}\bigskip |
|
32 \hrule\bigskip} |
|
33 \newenvironment{constants}{\begin{center}\small\begin{tabular}{rrrr}}{\end{tabular}\end{center}} |
|
34 |
|
35 \makeindex |
|
36 |
|
37 \underscoreoff |
|
38 |
|
39 \setcounter{secnumdepth}{2} \setcounter{tocdepth}{2} %% {secnumdepth}{2}??? |
|
40 |
|
41 \pagestyle{headings} |
|
42 \sloppy |
|
43 \binperiod %%%treat . like a binary operator |
|
44 |
|
45 \begin{document} |
|
46 \maketitle |
|
47 |
|
48 \begin{abstract} |
|
49 This manual describes Isabelle's formalizations of many-sorted first-order |
|
50 logic (\texttt{FOL}) and Zermelo-Fraenkel set theory (\texttt{ZF}). See the |
|
51 \emph{Reference Manual} for general Isabelle commands, and \emph{Introduction |
|
52 to Isabelle} for an overall tutorial. |
|
53 \end{abstract} |
|
54 |
|
55 \pagenumbering{roman} \tableofcontents \clearfirst |
|
56 \include{../Logics/syntax} |
|
57 \include{FOL} |
|
58 \include{ZF} |
|
59 \bibliographystyle{plain} |
|
60 \bibliography{string,general,atp,theory,funprog,logicprog,isabelle,crossref} |
|
61 \input{logics-ZF.ind} |
|
62 \end{document} |