doc-src/HOL/Makefile
author bulwahn
Fri, 09 Sep 2011 12:33:09 +0200
changeset 44854 0b3d3570ab31
parent 42628 50f257ea2aba
permissions -rw-r--r--
revisiting type annotations for Haskell: necessary type annotations are not inferred on the provided theorems but using the arguments and right hand sides, as these might differ in the case of constants with abstract code types


## targets

default: dvi


## dependencies

include ../Makefile.in

NAME = logics-HOL
FILES = logics-HOL.tex ../Logics/syntax.tex HOL.tex \
	 ../proof.sty ../iman.sty ../extra.sty ../ttbox.sty ../manual.bib

dvi: $(NAME).dvi

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

pdf: $(NAME).pdf

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