equal
deleted
inserted
replaced
9 FILES = tutorial.tex basics.tex fp.tex appendix.tex \ |
9 FILES = tutorial.tex basics.tex fp.tex appendix.tex \ |
10 ../iman.sty ttbox.sty extra.sty |
10 ../iman.sty ttbox.sty extra.sty |
11 |
11 |
12 tutorial.ps.gz: $(FILES) |
12 tutorial.ps.gz: $(FILES) |
13 isatool make |
13 isatool make |
14 -ln -sf ../gfx/isabelle_hol.eps . |
14 test -r isabelle_hol.eps || ln -s ../gfx/isabelle_hol.eps . |
15 -rm tutorial.dvi* |
15 -rm tutorial.dvi* |
16 latex tutorial |
16 latex tutorial |
17 bibtex tutorial |
17 bibtex tutorial |
18 latex tutorial |
18 latex tutorial |
19 latex tutorial |
19 latex tutorial |
21 latex tutorial |
21 latex tutorial |
22 dvips tutorial.dvi -o tutorial.ps |
22 dvips tutorial.dvi -o tutorial.ps |
23 gzip tutorial.ps |
23 gzip tutorial.ps |
24 |
24 |
25 dist: $(FILES) |
25 dist: $(FILES) |
26 -ln -sf ../gfx/isabelle_hol.eps . |
26 test -r isabelle_hol.eps || ln -s ../gfx/isabelle_hol.eps . |
27 -rm tutorial.dvi* |
27 -rm tutorial.dvi* |
28 latex tutorial |
28 latex tutorial |
29 latex tutorial |
29 latex tutorial |
30 ../sedindex tutorial |
30 ../sedindex tutorial |
31 latex tutorial |
31 latex tutorial |