diff -r 813ee27cd4d5 -r 8a96a64e0b35 doc-src/Logics/logics.tex
--- 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}