1.1 --- a/doc-src/ZF/logics-ZF.tex	Tue Aug 19 13:54:20 2003 +0200
     1.2 +++ b/doc-src/ZF/logics-ZF.tex	Tue Aug 19 18:45:48 2003 +0200
     1.3 @@ -1,8 +1,14 @@
     1.4  %% $Id$
     1.5  \documentclass[11pt,a4paper]{report}
     1.6 -\usepackage{graphicx,../iman,../extra,../ttbox,../proof,../rail,latexsym,../pdfsetup}
     1.7 +\usepackage{isabelle,isabellesym}
     1.8 +\usepackage{graphicx,logics,../ttbox,../proof,../rail,latexsym}
     1.9  
    1.10 -%%% to index derived rls:  ^\([a-zA-Z0-9][a-zA-Z0-9_]*\)        \\tdx{\1}  
    1.11 +\usepackage{../pdfsetup}   
    1.12 +%last package!
    1.13 +
    1.14 +\remarkstrue 
    1.15 +
    1.16 +%%% to index derived rls: ^\([a-zA-Z0-9][a-zA-Z0-9_]*\)        \\tdx{\1}  
    1.17  %%% to index rulenames:   ^ *(\([a-zA-Z0-9][a-zA-Z0-9_]*\),     \\tdx{\1}  
    1.18  %%% to index constants:   \\tt \([a-zA-Z0-9][a-zA-Z0-9_]*\)     \\cdx{\1}  
    1.19  %%% to deverbify:         \\verb|\([^|]*\)|     \\ttindex{\1}  
    1.20 @@ -13,20 +19,14 @@
    1.21  \author{{\em Lawrence C. Paulson}\\
    1.22          Computer Laboratory \\ University of Cambridge \\
    1.23          \texttt{lcp@cl.cam.ac.uk}\\[3ex] 
    1.24 -        With Contributions by Tobias Nipkow and Markus Wenzel%
    1.25 -\thanks{Markus Wenzel made numerous improvements.
    1.26 -    Philippe de Groote contributed to~ZF.  Philippe No\"el and
    1.27 -    Martin Coen made many contributions to~ZF.  The research has 
    1.28 -    been funded by the EPSRC (grants GR/G53279, GR/H40570, GR/K57381,
    1.29 -    GR/K77051, GR/M75440) and by ESPRIT (projects 3245:
    1.30 -    Logical Frameworks, and 6453: Types) and by the DFG Schwerpunktprogramm
    1.31 -    \emph{Deduktion}.}
    1.32 -}
    1.33 +        With Contributions by Tobias Nipkow and Markus Wenzel}
    1.34  
    1.35  \newcommand\subcaption[1]{\par {\centering\normalsize\sc#1\par}\bigskip
    1.36    \hrule\bigskip}
    1.37  \newenvironment{constants}{\begin{center}\small\begin{tabular}{rrrr}}{\end{tabular}\end{center}}
    1.38  
    1.39 +\let\ts=\thinspace
    1.40 +
    1.41  \makeindex
    1.42  
    1.43  \underscoreoff
    1.44 @@ -45,9 +45,30 @@
    1.45  logic (\texttt{FOL}) and Zermelo-Fraenkel set theory (\texttt{ZF}).  See the
    1.46  \emph{Reference Manual} for general Isabelle commands, and \emph{Introduction
    1.47    to Isabelle} for an overall tutorial.
    1.48 +
    1.49 +This manual is part of the earlier Isabelle documentation, 
    1.50 +which is somewhat superseded by the Isabelle/HOL
    1.51 +\emph{Tutorial}~\cite{isa-tutorial}. However, the present document is the
    1.52 +only available documentation for Isabelle's versions of first-order logic
    1.53 +and set theory. Much of it is concerned with 
    1.54 +the primitives for conducting proofs 
    1.55 +using the ML top level.  It has been rewritten to use the Isar proof
    1.56 +language, but evidence of the old \ML{} orientation remains.
    1.57  \end{abstract}
    1.58  
    1.59 -\pagenumbering{roman} \tableofcontents \clearfirst
    1.60 +
    1.61 +\subsubsection*{Acknowledgements} 
    1.62 +Markus Wenzel made numerous improvements.
    1.63 +    Philippe de Groote contributed to~ZF.  Philippe No\"el and
    1.64 +    Martin Coen made many contributions to~ZF.  The research has 
    1.65 +    been funded by the EPSRC (grants GR/G53279, GR/H40570, GR/K57381,
    1.66 +    GR/K77051, GR/M75440) and by ESPRIT (projects 3245:
    1.67 +    Logical Frameworks, and 6453: Types) and by the DFG Schwerpunktprogramm
    1.68 +    \emph{Deduktion}.
    1.69 +    
    1.70 +\pagenumbering{roman} \tableofcontents \cleardoublepage
    1.71 +\pagenumbering{arabic} 
    1.72 +\setcounter{page}{1} 
    1.73  \input{../Logics/syntax}
    1.74  \include{FOL}
    1.75  \include{ZF}