--- a/doc-src/Tutorial/tutorial.tex Mon May 10 17:07:19 1999 +0200
+++ b/doc-src/Tutorial/tutorial.tex Mon May 10 17:43:55 1999 +0200
@@ -1,6 +1,6 @@
\documentclass[11pt]{report}
-\usepackage{a4,latexsym,verbatim}
-\usepackage{graphicx}
+\usepackage{a4,latexsym,verbatim,graphicx,../pdfsetup}
+
\makeatletter
\input{../iman.sty}
@@ -39,13 +39,13 @@
%\binperiod %%%treat . like a binary operator
\begin{document}
-\title{\includegraphics[scale=.8]{isabelle_hol.eps}
+\title{\includegraphics[scale=.8]{isabelle_hol}
\\ \vspace{0.5cm} The Tutorial
\\ --- DRAFT ---}
\author{Tobias Nipkow\\
Technische Universit\"at M\"unchen \\
Institut f\"ur Informatik \\
-\texttt{http://www.in.tum.de/\~\relax nipkow/}}
+\url{http://www.in.tum.de/~nipkow/}}
\maketitle
\pagenumbering{roman}