doc-src/Tutorial/Makefile
author paulson
Fri, 27 Nov 1998 13:13:22 +0100
changeset 5980 2e9314c07146
parent 5548 5cd3396802f5
child 6600 5a94bd71cc41
permissions -rw-r--r--
added Real/Hyperreal
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
5376
60b31a24f1a6 *** empty log message ***
nipkow
parents:
diff changeset
     1
#  $Id$
60b31a24f1a6 *** empty log message ***
nipkow
parents:
diff changeset
     2
#########################################################################
60b31a24f1a6 *** empty log message ***
nipkow
parents:
diff changeset
     3
#									#
60b31a24f1a6 *** empty log message ***
nipkow
parents:
diff changeset
     4
#	Makefile for the report "Isabelle/HOL. The Tutorial"		#
60b31a24f1a6 *** empty log message ***
nipkow
parents:
diff changeset
     5
#									#
60b31a24f1a6 *** empty log message ***
nipkow
parents:
diff changeset
     6
#########################################################################
60b31a24f1a6 *** empty log message ***
nipkow
parents:
diff changeset
     7
60b31a24f1a6 *** empty log message ***
nipkow
parents:
diff changeset
     8
60b31a24f1a6 *** empty log message ***
nipkow
parents:
diff changeset
     9
FILES =  tutorial.tex basics.tex fp.tex appendix.tex \
60b31a24f1a6 *** empty log message ***
nipkow
parents:
diff changeset
    10
	 ../iman.sty ttbox.sty extra.sty
60b31a24f1a6 *** empty log message ***
nipkow
parents:
diff changeset
    11
60b31a24f1a6 *** empty log message ***
nipkow
parents:
diff changeset
    12
tutorial.ps.gz:   $(FILES)
60b31a24f1a6 *** empty log message ***
nipkow
parents:
diff changeset
    13
	isatool make
5548
5cd3396802f5 workaround for litte bug in our ln command
oheimb
parents: 5376
diff changeset
    14
	test -r isabelle_hol.eps || ln -s ../gfx/isabelle_hol.eps .
5376
60b31a24f1a6 *** empty log message ***
nipkow
parents:
diff changeset
    15
	-rm tutorial.dvi*
60b31a24f1a6 *** empty log message ***
nipkow
parents:
diff changeset
    16
	latex tutorial
60b31a24f1a6 *** empty log message ***
nipkow
parents:
diff changeset
    17
	bibtex tutorial
60b31a24f1a6 *** empty log message ***
nipkow
parents:
diff changeset
    18
	latex tutorial
60b31a24f1a6 *** empty log message ***
nipkow
parents:
diff changeset
    19
	latex tutorial
60b31a24f1a6 *** empty log message ***
nipkow
parents:
diff changeset
    20
	../sedindex tutorial
60b31a24f1a6 *** empty log message ***
nipkow
parents:
diff changeset
    21
	latex tutorial
60b31a24f1a6 *** empty log message ***
nipkow
parents:
diff changeset
    22
	dvips tutorial.dvi -o tutorial.ps
60b31a24f1a6 *** empty log message ***
nipkow
parents:
diff changeset
    23
	gzip tutorial.ps
60b31a24f1a6 *** empty log message ***
nipkow
parents:
diff changeset
    24
60b31a24f1a6 *** empty log message ***
nipkow
parents:
diff changeset
    25
dist:   $(FILES) 
5548
5cd3396802f5 workaround for litte bug in our ln command
oheimb
parents: 5376
diff changeset
    26
	test -r isabelle_hol.eps || ln -s ../gfx/isabelle_hol.eps .
5376
60b31a24f1a6 *** empty log message ***
nipkow
parents:
diff changeset
    27
	-rm tutorial.dvi*
60b31a24f1a6 *** empty log message ***
nipkow
parents:
diff changeset
    28
	latex tutorial
60b31a24f1a6 *** empty log message ***
nipkow
parents:
diff changeset
    29
	latex tutorial
60b31a24f1a6 *** empty log message ***
nipkow
parents:
diff changeset
    30
	../sedindex tutorial
60b31a24f1a6 *** empty log message ***
nipkow
parents:
diff changeset
    31
	latex tutorial
60b31a24f1a6 *** empty log message ***
nipkow
parents:
diff changeset
    32
60b31a24f1a6 *** empty log message ***
nipkow
parents:
diff changeset
    33
clean:
60b31a24f1a6 *** empty log message ***
nipkow
parents:
diff changeset
    34
	@rm *.aux *.log *.toc *.idx