doc-src/Logics/logics.tex

 %%% to index constants:   \\tt \([a-zA-Z0-9][a-zA-Z0-9_]*\)     \\idx{\1}  
 %%% to deverbify:         \\verb|\([^|]*\)|     \\ttindex{\1}  
 %% 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
     developed~\Modal{} with assistance from Rajeev Gor\'e.  The research
     has been funded by the SERC (grants GR/G53279, GR/H40570) and by ESPRIT

 \include{LK}
 %%\include{Modal}
 \include{CTT}
 %%\include{Cube}
 %%\include{LCF}
-\include{defining}
 \bibliographystyle{plain}
 \bibliography{atp,theory,funprog,logicprog,isabelle}
 \input{logics.ind}
 \end{document}