| author | wenzelm | 
| Thu, 19 Jul 2007 23:18:55 +0200 | |
| changeset 23868 | 8c6f2e7bfdb4 | 
| parent 23845 | 0b695c401d4d | 
| child 23927 | cbe0e4aeb53c | 
| permissions | -rw-r--r-- | 
| 8743 | 1 | # | 
| 2 | # $Id$ | |
| 3 | # | |
| 4 | ||
| 5 | ## targets | |
| 6 | ||
| 7 | default: dvi | |
| 8 | ||
| 9 | ||
| 10 | ## dependencies | |
| 11 | ||
| 12 | include ../Makefile.in | |
| 13 | ||
| 11430 | 14 | SEDINDEX = ./isa-index | 
| 11400 | 15 | |
| 8743 | 16 | NAME = tutorial | 
| 17 | FILES = tutorial.tex basics.tex fp.tex appendix.tex \ | |
| 11428 | 18 | Advanced/advanced.tex \ | 
| 19 | CTL/ctl.tex \ | |
| 23845 
0b695c401d4d
Replaced "hand-made" files by generated files in Inductive/document.
 berghofe parents: 
12677diff
changeset | 20 | Inductive/inductive.tex Inductive/document/AB.tex \ | 
| 
0b695c401d4d
Replaced "hand-made" files by generated files in Inductive/document.
 berghofe parents: 
12677diff
changeset | 21 | Inductive/document/Advanced.tex Inductive/document/Even.tex \ | 
| 
0b695c401d4d
Replaced "hand-made" files by generated files in Inductive/document.
 berghofe parents: 
12677diff
changeset | 22 | Inductive/document/Mutual.tex Inductive/document/Star.tex \ | 
| 11428 | 23 | Protocol/protocol.tex \ | 
| 24 | Rules/rules.tex Sets/sets.tex \ | |
| 12577 | 25 | Types/numerics.tex Types/types.tex \ | 
| 11647 
0538cb0f7999
initial setup for chapter on document preparation;
 wenzelm parents: 
11430diff
changeset | 26 | Documents/documents.tex \ | 
| 9695 | 27 | ../iman.sty ../ttbox.sty ../extra.sty \ | 
| 8847 | 28 | isabelle.sty isabellesym.sty ../pdfsetup.sty | 
| 8743 | 29 | |
| 30 | dvi: $(NAME).dvi | |
| 31 | ||
| 12677 | 32 | $(NAME).dvi: $(FILES) isabelle_hol.eps typedef.ps | 
| 8743 | 33 | $(LATEX) $(NAME) | 
| 34 | $(BIBTEX) $(NAME) | |
| 35 | $(LATEX) $(NAME) | |
| 36 | $(LATEX) $(NAME) | |
| 37 | $(SEDINDEX) $(NAME) | |
| 38 | $(LATEX) $(NAME) | |
| 39 | ||
| 40 | pdf: $(NAME).pdf | |
| 41 | ||
| 12677 | 42 | $(NAME).pdf: $(FILES) isabelle_hol.pdf typedef.pdf | 
| 8743 | 43 | $(PDFLATEX) $(NAME) | 
| 44 | $(BIBTEX) $(NAME) | |
| 45 | $(PDFLATEX) $(NAME) | |
| 46 | $(PDFLATEX) $(NAME) | |
| 47 | $(SEDINDEX) $(NAME) | |
| 48 | $(FIXBOOKMARKS) $(NAME).out | |
| 49 | $(PDFLATEX) $(NAME) | |
| 12672 | 50 | $(FIXBOOKMARKS) $(NAME).out |