diff -r 010dfaf75064 -r fc991461c7b9 doc-src/HOL/logics-HOL.tex
--- a/doc-src/HOL/logics-HOL.tex	Mon May 10 15:17:14 1999 +0200
+++ b/doc-src/HOL/logics-HOL.tex	Mon May 10 15:26:30 1999 +0200
@@ -14,7 +14,7 @@
 %%% to index constants:   \\tt \([a-zA-Z0-9][a-zA-Z0-9_]*\)     \\cdx{\1}  
 %%% to deverbify:         \\verb|\([^|]*\)|     \\ttindex{\1}  
 
-\title{\includegraphics[scale=0.5]{isabelle_hol.eps} \\[4ex] 
+\title{\includegraphics[scale=0.5]{isabelle_hol} \\[4ex] 
        Isabelle's Logics: HOL}
 
 \author{Tobias Nipkow\footnote
@@ -56,7 +56,7 @@
 \end{abstract}
 
 \pagenumbering{roman} \tableofcontents \clearfirst
-\include{../Logics/syntax}
+\input{../Logics/syntax}
 \include{HOL}
 \bibliographystyle{plain}
 \bibliography{../manual}