1.1 --- a/doc-src/Logics/logics.tex	Fri Jan 08 13:20:59 1999 +0100
     1.2 +++ b/doc-src/Logics/logics.tex	Fri Jan 08 14:02:04 1999 +0100
     1.3 @@ -1,3 +1,4 @@
     1.4 +%% $Id$
     1.5  \documentclass[12pt]{report}
     1.6  \usepackage{graphicx,a4,latexsym,../pdfsetup}
     1.7  
     1.8 @@ -8,15 +9,13 @@
     1.9  \input{../extra.sty}
    1.10  \makeatother
    1.11  
    1.12 -%% $Id$
    1.13  %%%STILL NEEDS MODAL, LCF
    1.14 -%%%\includeonly{ZF}
    1.15  %%% to index derived rls:  ^\([a-zA-Z0-9][a-zA-Z0-9_]*\)        \\tdx{\1}  
    1.16  %%% to index rulenames:   ^ *(\([a-zA-Z0-9][a-zA-Z0-9_]*\),     \\tdx{\1}  
    1.17  %%% to index constants:   \\tt \([a-zA-Z0-9][a-zA-Z0-9_]*\)     \\cdx{\1}  
    1.18  %%% to deverbify:         \\verb|\([^|]*\)|     \\ttindex{\1}  
    1.19  %% run    ../sedindex logics    to prepare index file
    1.20 -\title{\includegraphics[scale=0.5]{isabelle.eps} \\[4ex] Isabelle's Object-Logics}
    1.21 +\title{\includegraphics[scale=0.5]{isabelle.eps} \\[4ex] Isabelle's Logics}
    1.22  
    1.23  \author{{\em Lawrence C. Paulson}\\
    1.24          Computer Laboratory \\ University of Cambridge \\
    1.25 @@ -25,9 +24,8 @@
    1.26  \thanks{Tobias Nipkow revised and extended
    1.27      the chapter on \HOL.  Markus Wenzel made numerous improvements.
    1.28      Philippe de Groote wrote the
    1.29 -    first version of the logic~\LK{} and contributed to~\ZF{}.  Tobias
    1.30 -    Nipkow developed~\HOL{}, \LCF{} and~\Cube{}.  Philippe No\"el and
    1.31 -    Martin Coen made many contributions to~\ZF{}.  Martin Coen
    1.32 +    first version of the logic~\LK{}.  Tobias
    1.33 +    Nipkow developed~\HOL{}, \LCF{} and~\Cube{}.  Martin Coen
    1.34      developed~\Modal{} with assistance from Rajeev Gor\'e.  The research has 
    1.35      been funded by the EPSRC (grants GR/G53279, GR/H40570, GR/K57381,
    1.36      GR/K77051) and by ESPRIT project 6453: Types.}
    1.37 @@ -39,9 +37,6 @@
    1.38  
    1.39  \makeindex
    1.40  
    1.41 -%%\newenvironment{example}{\begin{Example}\rm}{\end{Example}}
    1.42 -%%\newtheorem{Example}{Example}[chapter]
    1.43 -
    1.44  \underscoreoff
    1.45  
    1.46  \setcounter{secnumdepth}{2} \setcounter{tocdepth}{2}  %% {secnumdepth}{2}???
    1.47 @@ -53,9 +48,8 @@
    1.48  \begin{document}
    1.49  \maketitle 
    1.50  \pagenumbering{roman} \tableofcontents \clearfirst
    1.51 -\include{intro}
    1.52 -\include{FOL}
    1.53 -\include{ZF}
    1.54 +\include{preface}
    1.55 +\include{syntax}
    1.56  \include{HOL}
    1.57  \include{LK}
    1.58  %%\include{Modal}