| 6600 |      1 | #
 | 
|  |      2 | # $Id$
 | 
|  |      3 | #
 | 
|  |      4 | 
 | 
|  |      5 | ## targets
 | 
|  |      6 | 
 | 
|  |      7 | default: dvi
 | 
| 5376 |      8 | 
 | 
|  |      9 | 
 | 
| 6600 |     10 | ## dependencies
 | 
|  |     11 | 
 | 
|  |     12 | include ../Makefile.in
 | 
|  |     13 | 
 | 
|  |     14 | NAME = tutorial
 | 
|  |     15 | FILES = tutorial.tex basics.tex fp.tex appendix.tex \
 | 
|  |     16 | 	../iman.sty ttbox.sty extra.sty
 | 
|  |     17 | 
 | 
|  |     18 | dvi: $(NAME).dvi
 | 
| 5376 |     19 | 
 | 
| 6600 |     20 | $(NAME).dvi: $(FILES) isabelle_hol.eps
 | 
|  |     21 | 	touch $(NAME).ind
 | 
|  |     22 | 	$(LATEX) $(NAME)
 | 
|  |     23 | 	$(BIBTEX) $(NAME)
 | 
|  |     24 | 	$(LATEX) $(NAME)
 | 
|  |     25 | 	$(LATEX) $(NAME)
 | 
|  |     26 | 	$(SEDINDEX) $(NAME)
 | 
|  |     27 | 	$(LATEX) $(NAME)
 | 
| 6628 |     28 | 
 | 
|  |     29 | pdf: $(NAME).pdf
 | 
|  |     30 | 
 | 
|  |     31 | $(NAME).pdf: $(FILES) isabelle_hol.pdf
 | 
|  |     32 | 	touch $(NAME).ind
 | 
|  |     33 | 	$(PDFLATEX) $(NAME)
 | 
|  |     34 | 	$(BIBTEX) $(NAME)
 | 
|  |     35 | 	$(PDFLATEX) $(NAME)
 | 
|  |     36 | 	$(PDFLATEX) $(NAME)
 | 
|  |     37 | 	$(SEDINDEX) $(NAME)
 | 
|  |     38 | 	$(FIXBOOKMARKS) $(NAME).out
 | 
|  |     39 | 	$(PDFLATEX) $(NAME)
 |