doc-src/TutorialI/Makefile
author nipkow
Sun, 22 Feb 2009 17:25:28 +0100
changeset 30056 0a35bee25c20
parent 26913 67040326ab7a
child 31676 4ee7a8af1903
permissions -rw-r--r--
added lemmas

#
# $Id$
#

## targets

default: dvi


## dependencies

include ../Makefile.in

SEDINDEX = ./isa-index

NAME = tutorial
FILES = tutorial.tex basics.tex fp.tex appendix.tex			\
	Advanced/advanced.tex CTL/ctl.tex Inductive/inductive.tex	\
	Inductive/document/AB.tex Inductive/document/Advanced.tex	\
	Inductive/document/Even.tex Inductive/document/Mutual.tex	\
	Inductive/document/Star.tex Protocol/protocol.tex		\
	Protocol/document/Event.tex Protocol/document/Message.tex	\
	Protocol/document/Public.tex Protocol/document/NS_Public.tex	\
	Rules/rules.tex Sets/sets.tex Types/numerics.tex		\
	Types/types.tex Documents/documents.tex ../iman.sty		\
	../ttbox.sty ../extra.sty ../isabelle.sty ../isabellesym.sty	\
	../pdfsetup.sty

dvi: $(NAME).dvi

$(NAME).dvi: $(FILES) isabelle_hol.eps typedef.ps
	$(LATEX) $(NAME)
	$(BIBTEX) $(NAME)
	$(LATEX) $(NAME)
	$(LATEX) $(NAME)
	$(SEDINDEX) $(NAME)
	$(LATEX) $(NAME)

pdf: $(NAME).pdf

$(NAME).pdf: $(FILES) isabelle_hol.pdf typedef.pdf
	$(PDFLATEX) $(NAME)
	$(BIBTEX) $(NAME)
	$(PDFLATEX) $(NAME)
	$(PDFLATEX) $(NAME)
	$(SEDINDEX) $(NAME)
	$(FIXBOOKMARKS) $(NAME).out
	$(PDFLATEX) $(NAME)
	$(FIXBOOKMARKS) $(NAME).out