| 8743 |      1 | 
 | 
|  |      2 | ## targets
 | 
|  |      3 | 
 | 
|  |      4 | default: dvi
 | 
|  |      5 | 
 | 
|  |      6 | 
 | 
|  |      7 | ## dependencies
 | 
|  |      8 | 
 | 
|  |      9 | include ../Makefile.in
 | 
|  |     10 | 
 | 
| 11430 |     11 | SEDINDEX = ./isa-index
 | 
| 11400 |     12 | 
 | 
| 8743 |     13 | NAME = tutorial
 | 
| 26913 |     14 | FILES = tutorial.tex basics.tex fp.tex appendix.tex			\
 | 
|  |     15 | 	Advanced/advanced.tex CTL/ctl.tex Inductive/inductive.tex	\
 | 
|  |     16 | 	Inductive/document/AB.tex Inductive/document/Advanced.tex	\
 | 
|  |     17 | 	Inductive/document/Even.tex Inductive/document/Mutual.tex	\
 | 
|  |     18 | 	Inductive/document/Star.tex Protocol/protocol.tex		\
 | 
|  |     19 | 	Protocol/document/Event.tex Protocol/document/Message.tex	\
 | 
|  |     20 | 	Protocol/document/Public.tex Protocol/document/NS_Public.tex	\
 | 
|  |     21 | 	Rules/rules.tex Sets/sets.tex Types/numerics.tex		\
 | 
| 31676 |     22 | 	Types/types.tex Types/document/Overloading.tex \
 | 
|  |     23 | 	Types/document/Axioms.tex Documents/documents.tex Misc/document/appendix.tex ../iman.sty	\
 | 
| 42511 |     24 | 	../ttbox.sty ../extra.sty ../../lib/texinputs/isabelle.sty ../../lib/texinputs/isabellesym.sty	\
 | 
| 26913 |     25 | 	../pdfsetup.sty
 | 
| 8743 |     26 | 
 | 
|  |     27 | dvi: $(NAME).dvi
 | 
|  |     28 | 
 | 
| 12677 |     29 | $(NAME).dvi: $(FILES) isabelle_hol.eps typedef.ps
 | 
| 8743 |     30 | 	$(LATEX) $(NAME)
 | 
|  |     31 | 	$(BIBTEX) $(NAME)
 | 
|  |     32 | 	$(LATEX) $(NAME)
 | 
|  |     33 | 	$(LATEX) $(NAME)
 | 
|  |     34 | 	$(SEDINDEX) $(NAME)
 | 
|  |     35 | 	$(LATEX) $(NAME)
 | 
|  |     36 | 
 | 
|  |     37 | pdf: $(NAME).pdf
 | 
|  |     38 | 
 | 
| 12677 |     39 | $(NAME).pdf: $(FILES) isabelle_hol.pdf typedef.pdf
 | 
| 8743 |     40 | 	$(PDFLATEX) $(NAME)
 | 
|  |     41 | 	$(BIBTEX) $(NAME)
 | 
|  |     42 | 	$(PDFLATEX) $(NAME)
 | 
|  |     43 | 	$(PDFLATEX) $(NAME)
 | 
|  |     44 | 	$(SEDINDEX) $(NAME)
 | 
|  |     45 | 	$(FIXBOOKMARKS) $(NAME).out
 | 
|  |     46 | 	$(PDFLATEX) $(NAME)
 | 
| 12672 |     47 | 	$(FIXBOOKMARKS) $(NAME).out
 |