paulson@6121: %% $Id$
paulson@8248: \documentclass[11pt,a4paper]{report}
wenzelm@26913: \usepackage{../isabelle,../isabellesym}
paulson@14154: \usepackage{graphicx,logics,../ttbox,../proof,../rail,latexsym}
paulson@6121: 
paulson@14154: \usepackage{../pdfsetup}   
paulson@14154: %last package!
paulson@14154: 
paulson@14154: \remarkstrue 
paulson@14154: 
paulson@14154: %%% to index derived rls: ^\([a-zA-Z0-9][a-zA-Z0-9_]*\)        \\tdx{\1}  
paulson@6121: %%% to index rulenames:   ^ *(\([a-zA-Z0-9][a-zA-Z0-9_]*\),     \\tdx{\1}  
paulson@6121: %%% to index constants:   \\tt \([a-zA-Z0-9][a-zA-Z0-9_]*\)     \\cdx{\1}  
paulson@6121: %%% to deverbify:         \\verb|\([^|]*\)|     \\ttindex{\1}  
paulson@6121: 
wenzelm@6579: \title{\includegraphics[scale=0.5]{isabelle_zf} \\[4ex] 
paulson@6121:        Isabelle's Logics: FOL and ZF}
paulson@6121: 
paulson@6121: \author{{\em Lawrence C. Paulson}\\
paulson@6121:         Computer Laboratory \\ University of Cambridge \\
paulson@6121:         \texttt{lcp@cl.cam.ac.uk}\\[3ex] 
paulson@14154:         With Contributions by Tobias Nipkow and Markus Wenzel}
paulson@6121: 
paulson@6121: \newcommand\subcaption[1]{\par {\centering\normalsize\sc#1\par}\bigskip
paulson@6121:   \hrule\bigskip}
paulson@6121: \newenvironment{constants}{\begin{center}\small\begin{tabular}{rrrr}}{\end{tabular}\end{center}}
paulson@6121: 
paulson@14154: \let\ts=\thinspace
paulson@14154: 
paulson@6121: \makeindex
paulson@6121: 
paulson@6121: \underscoreoff
paulson@6121: 
paulson@6121: \setcounter{secnumdepth}{2} \setcounter{tocdepth}{2}  %% {secnumdepth}{2}???
paulson@6121: 
paulson@6121: \pagestyle{headings}
paulson@6121: \sloppy
paulson@6121: \binperiod     %%%treat . like a binary operator
paulson@6121: 
paulson@6121: \begin{document}
paulson@6121: \maketitle 
paulson@6121: 
paulson@6121: \begin{abstract}
paulson@6121: This manual describes Isabelle's formalizations of many-sorted first-order
paulson@6121: logic (\texttt{FOL}) and Zermelo-Fraenkel set theory (\texttt{ZF}).  See the
paulson@6121: \emph{Reference Manual} for general Isabelle commands, and \emph{Introduction
paulson@6121:   to Isabelle} for an overall tutorial.
paulson@14154: 
paulson@14154: This manual is part of the earlier Isabelle documentation, 
paulson@14154: which is somewhat superseded by the Isabelle/HOL
paulson@14154: \emph{Tutorial}~\cite{isa-tutorial}. However, the present document is the
paulson@14154: only available documentation for Isabelle's versions of first-order logic
paulson@14154: and set theory. Much of it is concerned with 
paulson@14154: the primitives for conducting proofs 
paulson@14154: using the ML top level.  It has been rewritten to use the Isar proof
paulson@14154: language, but evidence of the old \ML{} orientation remains.
paulson@6121: \end{abstract}
paulson@6121: 
paulson@14154: 
paulson@14154: \subsubsection*{Acknowledgements} 
paulson@14154: Markus Wenzel made numerous improvements.
paulson@14154:     Philippe de Groote contributed to~ZF.  Philippe No\"el and
paulson@14154:     Martin Coen made many contributions to~ZF.  The research has 
paulson@14154:     been funded by the EPSRC (grants GR/G53279, GR/H40570, GR/K57381,
paulson@14154:     GR/K77051, GR/M75440) and by ESPRIT (projects 3245:
paulson@14154:     Logical Frameworks, and 6453: Types) and by the DFG Schwerpunktprogramm
paulson@14154:     \emph{Deduktion}.
paulson@14154:     
paulson@14154: \pagenumbering{roman} \tableofcontents \cleardoublepage
paulson@14154: \pagenumbering{arabic} 
paulson@14154: \setcounter{page}{1} 
wenzelm@6623: \input{../Logics/syntax}
paulson@6121: \include{FOL}
paulson@6121: \include{ZF}
paulson@6121: \bibliographystyle{plain}
paulson@6592: \bibliography{../manual}
wenzelm@8828: \printindex
paulson@6121: \end{document}