--- a/doc-src/Logics/logics.tex Fri Apr 15 13:33:19 1994 +0200
+++ b/doc-src/Logics/logics.tex Fri Apr 15 14:09:12 1994 +0200
@@ -9,9 +9,8 @@
%% run ../sedindex logics to prepare index file
\title{Isabelle's Object-Logics}
-\author{{\em Lawrence C. Paulson}\thanks{Tobias Nipkow and Markus Wenzel,
- of T. U. Munich, wrote the chapter `Defining Logics'. Markus Wenzel
- also suggested changes and corrections. Philippe de Groote wrote the
+\author{{\em Lawrence C. Paulson}\thanks{Tobias Nipkow and Markus Wenzel
+ suggested changes and corrections. 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
@@ -57,7 +56,6 @@
\include{CTT}
%%\include{Cube}
%%\include{LCF}
-\include{defining}
\bibliographystyle{plain}
\bibliography{atp,theory,funprog,logicprog,isabelle}
\input{logics.ind}