1.1 --- a/doc-src/HOL/Makefile	Mon May 10 15:17:14 1999 +0200
     1.2 +++ b/doc-src/HOL/Makefile	Mon May 10 15:26:30 1999 +0200
     1.3 @@ -27,3 +27,17 @@
     1.4  	$(LATEX) $(NAME)
     1.5  	$(SEDINDEX) $(NAME)
     1.6  	$(LATEX) $(NAME)
     1.7 +
     1.8 +
     1.9 +pdf: $(NAME).pdf
    1.10 +
    1.11 +$(NAME).pdf: $(FILES) isabelle_hol.pdf
    1.12 +	touch $(NAME).ind
    1.13 +	$(PDFLATEX) $(NAME)
    1.14 +	$(RAIL) $(NAME)
    1.15 +	$(BIBTEX) $(NAME)
    1.16 +	$(PDFLATEX) $(NAME)
    1.17 +	$(PDFLATEX) $(NAME)
    1.18 +	$(SEDINDEX) $(NAME)
    1.19 +	$(FIXBOOKMARKS) $(NAME).out
    1.20 +	$(PDFLATEX) $(NAME)