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