doc-src/Tutorial/Makefile
author nipkow
Wed, 26 Aug 1998 17:27:27 +0200
changeset 5377 efb799c5ed3c
parent 5376 60b31a24f1a6
child 5548 5cd3396802f5
permissions -rw-r--r--
*** empty log message ***

#  $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