--- a/doc-src/Logics/logics.tex Tue May 04 18:04:45 1999 +0200
+++ b/doc-src/Logics/logics.tex Tue May 04 18:05:34 1999 +0200
@@ -21,15 +21,12 @@
Computer Laboratory \\ University of Cambridge \\
\texttt{lcp@cl.cam.ac.uk}\\[3ex]
With Contributions by Tobias Nipkow and Markus Wenzel%
-\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{}. 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.}
-}
+ \thanks{Markus Wenzel made numerous improvements. Philippe de Groote
+ wrote the first version of the logic~\LK{}. Tobias Nipkow developed
+ \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.} }
\newcommand\subcaption[1]{\par {\centering\normalsize\sc#1\par}\bigskip
\hrule\bigskip}
@@ -50,13 +47,12 @@
\pagenumbering{roman} \tableofcontents \clearfirst
\include{preface}
\include{syntax}
-\include{HOL}
\include{LK}
%%\include{Modal}
\include{CTT}
%%\include{Cube}
%%\include{LCF}
\bibliographystyle{plain}
-\bibliography{string,general,atp,theory,funprog,logicprog,isabelle,crossref}
+\bibliography{bib,string,general,atp,theory,funprog,logicprog,isabelle,crossref}
\input{logics.ind}
\end{document}