doc-src/ZF/logics-ZF.tex
author wenzelm
Sun May 01 16:36:34 2011 +0200 (2011-05-01)
changeset 42511 bf89455ccf9d
parent 26913 67040326ab7a
child 42622 61a99eb5eb9d
permissions -rw-r--r--
eliminated copies of isabelle style files;
     1 %% $Id$
     2 \documentclass[11pt,a4paper]{report}
     3 \usepackage{../../lib/texinputs/isabelle,../../lib/texinputs/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}