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