1 \documentclass[11pt,a4paper]{report}
2 \usepackage{../../lib/texinputs/isabelle,../../lib/texinputs/isabellesym}
3 \usepackage{graphicx,logics,../ttbox,../proof,latexsym}
5 \usepackage{../pdfsetup}
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}
15 \title{\includegraphics[scale=0.5]{isabelle_zf} \\[4ex]
16 Isabelle's Logics: FOL and ZF}
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}
23 \newcommand\subcaption[1]{\par {\centering\normalsize\sc#1\par}\bigskip
25 \newenvironment{constants}{\begin{center}\small\begin{tabular}{rrrr}}{\end{tabular}\end{center}}
33 \setcounter{secnumdepth}{2} \setcounter{tocdepth}{2} %% {secnumdepth}{2}???
37 \binperiod %%%treat . like a binary operator
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.
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.
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
68 \pagenumbering{roman} \tableofcontents \cleardoublepage
69 \pagenumbering{arabic}
71 \input{../Logics/syntax}
74 \bibliographystyle{plain}
75 \bibliography{../manual}