--- 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}