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