1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/doc-src/Tutorial/Makefile	Wed Aug 26 17:11:29 1998 +0200
     1.3 @@ -0,0 +1,34 @@
     1.4 +#  $Id$
     1.5 +#########################################################################
     1.6 +#									#
     1.7 +#	Makefile for the report "Isabelle/HOL. The Tutorial"		#
     1.8 +#									#
     1.9 +#########################################################################
    1.10 +
    1.11 +
    1.12 +FILES =  tutorial.tex basics.tex fp.tex appendix.tex \
    1.13 +	 ../iman.sty ttbox.sty extra.sty
    1.14 +
    1.15 +tutorial.ps.gz:   $(FILES)
    1.16 +	isatool make
    1.17 +	-ln -sf ../gfx/isabelle_hol.eps .
    1.18 +	-rm tutorial.dvi*
    1.19 +	latex tutorial
    1.20 +	bibtex tutorial
    1.21 +	latex tutorial
    1.22 +	latex tutorial
    1.23 +	../sedindex tutorial
    1.24 +	latex tutorial
    1.25 +	dvips tutorial.dvi -o tutorial.ps
    1.26 +	gzip tutorial.ps
    1.27 +
    1.28 +dist:   $(FILES) 
    1.29 +	-ln -sf ../gfx/isabelle_hol.eps .
    1.30 +	-rm tutorial.dvi*
    1.31 +	latex tutorial
    1.32 +	latex tutorial
    1.33 +	../sedindex tutorial
    1.34 +	latex tutorial
    1.35 +
    1.36 +clean:
    1.37 +	@rm *.aux *.log *.toc *.idx

     2.1 --- a/doc-src/Tutorial/tutorial.tex	Wed Aug 26 16:57:49 1998 +0200
     2.2 +++ b/doc-src/Tutorial/tutorial.tex	Wed Aug 26 17:11:29 1998 +0200
     2.3 @@ -39,7 +39,7 @@
     2.4  %\binperiod     %%%treat . like a binary operator
     2.5  
     2.6  \begin{document}
     2.7 -\title{\includegraphics[scale=0.2,angle=-90]{isabelle_hol.ps}
     2.8 +\title{\includegraphics[scale=.8]{isabelle_hol.eps}
     2.9         \\ \vspace{0.5cm} The Tutorial
    2.10         \\ --- DRAFT ---}
    2.11  \author{Tobias Nipkow\\