doc-src/ZF/logics-ZF.tex
 author haftmann Tue Oct 10 13:59:12 2006 +0200 (2006-10-10) changeset 20950 981fa0ce23ed parent 14154 3bc0128e2c74 child 26913 67040326ab7a permissions -rw-r--r--
     1 %% $Id$

     2 \documentclass[11pt,a4paper]{report}

     3 \usepackage{isabelle,isabellesym}

     4 \usepackage{graphicx,logics,../ttbox,../proof,../rail,latexsym}

     5

     6 \usepackage{../pdfsetup}

     7 %last package!

     8

     9 \remarkstrue

    10

    11 %%% to index derived rls: ^$$[a-zA-Z0-9][a-zA-Z0-9_]*$$        \\tdx{\1}

    12 %%% to index rulenames:   ^ *($$[a-zA-Z0-9][a-zA-Z0-9_]*$$,     \\tdx{\1}

    13 %%% to index constants:   \\tt $$[a-zA-Z0-9][a-zA-Z0-9_]*$$     \\cdx{\1}

    14 %%% to deverbify:         \\verb|$$[^|]*$$|     \\ttindex{\1}

    15

    16 \title{\includegraphics[scale=0.5]{isabelle_zf} \\[4ex]

    17        Isabelle's Logics: FOL and ZF}

    18

    19 \author{{\em Lawrence C. Paulson}\\

    20         Computer Laboratory \\ University of Cambridge \\

    21         \texttt{lcp@cl.cam.ac.uk}\\[3ex]

    22         With Contributions by Tobias Nipkow and Markus Wenzel}

    23

    24 \newcommand\subcaption[1]{\par {\centering\normalsize\sc#1\par}\bigskip

    25   \hrule\bigskip}

    26 \newenvironment{constants}{\begin{center}\small\begin{tabular}{rrrr}}{\end{tabular}\end{center}}

    27

    28 \let\ts=\thinspace

    29

    30 \makeindex

    31

    32 \underscoreoff

    33

    34 \setcounter{secnumdepth}{2} \setcounter{tocdepth}{2}  %% {secnumdepth}{2}???

    35

    36 \pagestyle{headings}

    37 \sloppy

    38 \binperiod     %%%treat . like a binary operator

    39

    40 \begin{document}

    41 \maketitle

    42

    43 \begin{abstract}

    44 This manual describes Isabelle's formalizations of many-sorted first-order

    45 logic (\texttt{FOL}) and Zermelo-Fraenkel set theory (\texttt{ZF}).  See the

    46 \emph{Reference Manual} for general Isabelle commands, and \emph{Introduction

    47   to Isabelle} for an overall tutorial.

    48

    49 This manual is part of the earlier Isabelle documentation,

    50 which is somewhat superseded by the Isabelle/HOL

    51 \emph{Tutorial}~\cite{isa-tutorial}. However, the present document is the

    52 only available documentation for Isabelle's versions of first-order logic

    53 and set theory. Much of it is concerned with

    54 the primitives for conducting proofs

    55 using the ML top level.  It has been rewritten to use the Isar proof

    56 language, but evidence of the old \ML{} orientation remains.

    57 \end{abstract}

    58

    59

    60 \subsubsection*{Acknowledgements}

    61 Markus Wenzel made numerous improvements.

    62     Philippe de Groote contributed to~ZF.  Philippe No\"el and

    63     Martin Coen made many contributions to~ZF.  The research has

    64     been funded by the EPSRC (grants GR/G53279, GR/H40570, GR/K57381,

    65     GR/K77051, GR/M75440) and by ESPRIT (projects 3245:

    66     Logical Frameworks, and 6453: Types) and by the DFG Schwerpunktprogramm

    67     \emph{Deduktion}.

    68

    69 \pagenumbering{roman} \tableofcontents \cleardoublepage

    70 \pagenumbering{arabic}

    71 \setcounter{page}{1}

    72 \input{../Logics/syntax}

    73 \include{FOL}

    74 \include{ZF}

    75 \bibliographystyle{plain}

    76 \bibliography{../manual}

    77 \printindex

    78 \end{document}