1 \documentclass[11pt,a4paper]{report} |
|
2 \usepackage{../../lib/texinputs/isabelle,../../lib/texinputs/isabellesym} |
|
3 \usepackage{graphicx,logics,../ttbox,../proof,latexsym} |
|
4 |
|
5 \usepackage{../pdfsetup} |
|
6 %last package! |
|
7 |
|
8 \remarkstrue |
|
9 |
|
10 %%% to index derived rls: ^\([a-zA-Z0-9][a-zA-Z0-9_]*\) \\tdx{\1} |
|
11 %%% to index rulenames: ^ *(\([a-zA-Z0-9][a-zA-Z0-9_]*\), \\tdx{\1} |
|
12 %%% to index constants: \\tt \([a-zA-Z0-9][a-zA-Z0-9_]*\) \\cdx{\1} |
|
13 %%% to deverbify: \\verb|\([^|]*\)| \\ttindex{\1} |
|
14 |
|
15 \title{\includegraphics[scale=0.5]{isabelle_zf} \\[4ex] |
|
16 Isabelle's Logics: FOL and ZF} |
|
17 |
|
18 \author{{\em Lawrence C. Paulson}\\ |
|
19 Computer Laboratory \\ University of Cambridge \\ |
|
20 \texttt{lcp@cl.cam.ac.uk}\\[3ex] |
|
21 With Contributions by Tobias Nipkow and Markus Wenzel} |
|
22 |
|
23 \newcommand\subcaption[1]{\par {\centering\normalsize\sc#1\par}\bigskip |
|
24 \hrule\bigskip} |
|
25 \newenvironment{constants}{\begin{center}\small\begin{tabular}{rrrr}}{\end{tabular}\end{center}} |
|
26 |
|
27 \let\ts=\thinspace |
|
28 |
|
29 \makeindex |
|
30 |
|
31 \underscoreoff |
|
32 |
|
33 \setcounter{secnumdepth}{2} \setcounter{tocdepth}{2} %% {secnumdepth}{2}??? |
|
34 |
|
35 \pagestyle{headings} |
|
36 \sloppy |
|
37 \binperiod %%%treat . like a binary operator |
|
38 |
|
39 \begin{document} |
|
40 \maketitle |
|
41 |
|
42 \begin{abstract} |
|
43 This manual describes Isabelle's formalizations of many-sorted first-order |
|
44 logic (\texttt{FOL}) and Zermelo-Fraenkel set theory (\texttt{ZF}). See the |
|
45 \emph{Reference Manual} for general Isabelle commands, and \emph{Introduction |
|
46 to Isabelle} for an overall tutorial. |
|
47 |
|
48 This manual is part of the earlier Isabelle documentation, |
|
49 which is somewhat superseded by the Isabelle/HOL |
|
50 \emph{Tutorial}~\cite{isa-tutorial}. However, the present document is the |
|
51 only available documentation for Isabelle's versions of first-order logic |
|
52 and set theory. Much of it is concerned with |
|
53 the primitives for conducting proofs |
|
54 using the ML top level. It has been rewritten to use the Isar proof |
|
55 language, but evidence of the old \ML{} orientation remains. |
|
56 \end{abstract} |
|
57 |
|
58 |
|
59 \subsubsection*{Acknowledgements} |
|
60 Markus Wenzel made numerous improvements. |
|
61 Philippe de Groote contributed to~ZF. Philippe No\"el and |
|
62 Martin Coen made many contributions to~ZF. The research has |
|
63 been funded by the EPSRC (grants GR/G53279, GR/H40570, GR/K57381, |
|
64 GR/K77051, GR/M75440) and by ESPRIT (projects 3245: |
|
65 Logical Frameworks, and 6453: Types) and by the DFG Schwerpunktprogramm |
|
66 \emph{Deduktion}. |
|
67 |
|
68 \pagenumbering{roman} \tableofcontents \cleardoublepage |
|
69 \pagenumbering{arabic} |
|
70 \setcounter{page}{1} |
|
71 \input{../Logics/syntax} |
|
72 \include{FOL} |
|
73 \include{ZF} |
|
74 \bibliographystyle{plain} |
|
75 \bibliography{../manual} |
|
76 \printindex |
|
77 \end{document} |
|