# HG changeset patch
# User nipkow
# Date 904144289 -7200
# Node ID 60b31a24f1a6e104ffb96f800bb29e5097bbc4a6
# Parent  1463e182c5331d17ddd758287f00fd6dd0b7f7cd
*** empty log message ***

diff -r 1463e182c533 -r 60b31a24f1a6 doc-src/Tutorial/Makefile
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Tutorial/Makefile	Wed Aug 26 17:11:29 1998 +0200
@@ -0,0 +1,34 @@
+#  $Id$
+#########################################################################
+#									#
+#	Makefile for the report "Isabelle/HOL. The Tutorial"		#
+#									#
+#########################################################################
+
+
+FILES =  tutorial.tex basics.tex fp.tex appendix.tex \
+	 ../iman.sty ttbox.sty extra.sty
+
+tutorial.ps.gz:   $(FILES)
+	isatool make
+	-ln -sf ../gfx/isabelle_hol.eps .
+	-rm tutorial.dvi*
+	latex tutorial
+	bibtex tutorial
+	latex tutorial
+	latex tutorial
+	../sedindex tutorial
+	latex tutorial
+	dvips tutorial.dvi -o tutorial.ps
+	gzip tutorial.ps
+
+dist:   $(FILES) 
+	-ln -sf ../gfx/isabelle_hol.eps .
+	-rm tutorial.dvi*
+	latex tutorial
+	latex tutorial
+	../sedindex tutorial
+	latex tutorial
+
+clean:
+	@rm *.aux *.log *.toc *.idx
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\\