--- 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}