| changeset 9695 | ec7d7f877712 |
| parent 8828 | 5be2d1745c61 |
| 9694:13f3aaf12be2 | 9695:ec7d7f877712 |
|---|---|
11 |
11 |
12 include ../Makefile.in |
12 include ../Makefile.in |
13 |
13 |
14 NAME = tutorial |
14 NAME = tutorial |
15 FILES = tutorial.tex basics.tex fp.tex appendix.tex \ |
15 FILES = tutorial.tex basics.tex fp.tex appendix.tex \ |
16 ../iman.sty ttbox.sty extra.sty |
16 ../iman.sty ../ttbox.sty ../extra.sty |
17 |
17 |
18 dvi: $(NAME).dvi |
18 dvi: $(NAME).dvi |
19 |
19 |
20 $(NAME).dvi: $(FILES) isabelle_hol.eps |
20 $(NAME).dvi: $(FILES) isabelle_hol.eps |
21 $(LATEX) $(NAME) |
21 $(LATEX) $(NAME) |