
diff -r 1463e182c533 -r 60b31a24f1a6 doc-src/Tutorial/tutorial.tex
--- a/doc-src/Tutorial/tutorial.tex	Wed Aug 26 16:57:49 1998 +0200
+++ b/doc-src/Tutorial/tutorial.tex	Wed Aug 26 17:11:29 1998 +0200
@@ -39,7 +39,7 @@
 %\binperiod     %%%treat . like a binary operator
 
 \begin{document}
-\title{\includegraphics[scale=0.2,angle=-90]{isabelle_hol.ps}
+\title{\includegraphics[scale=.8]{isabelle_hol.eps}
        \\ \vspace{0.5cm} The Tutorial
        \\ --- DRAFT ---}
 \author{Tobias Nipkow\\




