
diff -r 1b2392ac5752 -r 5583261db33d doc-src/Logics/logics.tex
--- a/doc-src/Logics/logics.tex	Fri Jan 08 13:20:59 1999 +0100
+++ b/doc-src/Logics/logics.tex	Fri Jan 08 14:02:04 1999 +0100
@@ -1,3 +1,4 @@
+%% $Id$
 \documentclass[12pt]{report}
 \usepackage{graphicx,a4,latexsym,../pdfsetup}
 
@@ -8,15 +9,13 @@
 \input{../extra.sty}
 \makeatother
 
-%% $Id$
 %%%STILL NEEDS MODAL, LCF
-%%%\includeonly{ZF}
 %%% to index derived rls:  ^\([a-zA-Z0-9][a-zA-Z0-9_]*\)        \\tdx{\1}  
 %%% to index rulenames:   ^ *(\([a-zA-Z0-9][a-zA-Z0-9_]*\),     \\tdx{\1}  
 %%% to index constants:   \\tt \([a-zA-Z0-9][a-zA-Z0-9_]*\)     \\cdx{\1}  
 %%% to deverbify:         \\verb|\([^|]*\)|     \\ttindex{\1}  
 %% run    ../sedindex logics    to prepare index file
-\title{\includegraphics[scale=0.5]{isabelle.eps} \\[4ex] Isabelle's Object-Logics}
+\title{\includegraphics[scale=0.5]{isabelle.eps} \\[4ex] Isabelle's Logics}
 
 \author{{\em Lawrence C. Paulson}\\
         Computer Laboratory \\ University of Cambridge \\
@@ -25,9 +24,8 @@
 \thanks{Tobias Nipkow revised and extended
     the chapter on \HOL.  Markus Wenzel made numerous improvements.
     Philippe de Groote wrote the
-    first version of the logic~\LK{} and contributed to~\ZF{}.  Tobias
-    Nipkow developed~\HOL{}, \LCF{} and~\Cube{}.  Philippe No\"el and
-    Martin Coen made many contributions to~\ZF{}.  Martin Coen
+    first version of the logic~\LK{}.  Tobias
+    Nipkow developed~\HOL{}, \LCF{} and~\Cube{}.  Martin Coen
     developed~\Modal{} with assistance from Rajeev Gor\'e.  The research has 
     been funded by the EPSRC (grants GR/G53279, GR/H40570, GR/K57381,
     GR/K77051) and by ESPRIT project 6453: Types.}
@@ -39,9 +37,6 @@
 
 \makeindex
 
-%%\newenvironment{example}{\begin{Example}\rm}{\end{Example}}
-%%\newtheorem{Example}{Example}[chapter]
-
 \underscoreoff
 
 \setcounter{secnumdepth}{2} \setcounter{tocdepth}{2}  %% {secnumdepth}{2}???
@@ -53,9 +48,8 @@
 \begin{document}
 \maketitle 
 \pagenumbering{roman} \tableofcontents \clearfirst
-\include{intro}
-\include{FOL}
-\include{ZF}
+\include{preface}
+\include{syntax}
 \include{HOL}
 \include{LK}
 %%\include{Modal}




