doc-src/TutorialI/Makefile
changeset 49537 708278fc2dff
parent 43508 381fdcab0f36
child 49627 795d38a6dab3
equal deleted inserted replaced
49536:0e4bb86c74fd 49537:708278fc2dff
    11 SEDINDEX = ./isa-index
    11 SEDINDEX = ./isa-index
    12 
    12 
    13 NAME = tutorial
    13 NAME = tutorial
    14 FILES = tutorial.tex basics.tex fp.tex appendix.tex			\
    14 FILES = tutorial.tex basics.tex fp.tex appendix.tex			\
    15 	Advanced/advanced.tex CTL/ctl.tex Inductive/inductive.tex	\
    15 	Advanced/advanced.tex CTL/ctl.tex Inductive/inductive.tex	\
    16 	Inductive/document/AB.tex Inductive/document/Advanced.tex	\
    16 	document/AB.tex document/Advanced.tex document/Even.tex		\
    17 	Inductive/document/Even.tex Inductive/document/Mutual.tex	\
    17 	document/Mutual.tex document/Star.tex Protocol/protocol.tex	\
    18 	Inductive/document/Star.tex Protocol/protocol.tex		\
    18 	document/Event.tex document/Message.tex document/Public.tex	\
    19 	Protocol/document/Event.tex Protocol/document/Message.tex	\
    19 	document/NS_Public.tex Rules/rules.tex Sets/sets.tex		\
    20 	Protocol/document/Public.tex Protocol/document/NS_Public.tex	\
    20 	Types/numerics.tex Types/types.tex document/Overloading.tex	\
    21 	Rules/rules.tex Sets/sets.tex Types/numerics.tex		\
    21 	document/Axioms.tex Documents/documents.tex			\
    22 	Types/types.tex Types/document/Overloading.tex \
    22 	document/appendix.tex ../iman.sty ../ttbox.sty ../extra.sty	\
    23 	Types/document/Axioms.tex Documents/documents.tex Misc/document/appendix.tex ../iman.sty	\
    23 	../../lib/texinputs/isabelle.sty				\
    24 	../ttbox.sty ../extra.sty ../../lib/texinputs/isabelle.sty ../../lib/texinputs/isabellesym.sty	\
    24 	../../lib/texinputs/isabellesym.sty ../pdfsetup.sty
    25 	../pdfsetup.sty
       
    26 
    25 
    27 dvi: $(NAME).dvi
    26 dvi: $(NAME).dvi
    28 
    27 
    29 $(NAME).dvi: $(FILES) isabelle_hol.eps typedef.ps
    28 $(NAME).dvi: $(FILES) isabelle_hol.eps typedef.ps
    30 	$(LATEX) $(NAME)
    29 	$(LATEX) $(NAME)