diff -r c2511c9ea37e -r 12ed4f748f7c doc-src/Tutorial/Makefile
--- a/doc-src/Tutorial/Makefile	Mon May 10 17:07:19 1999 +0200
+++ b/doc-src/Tutorial/Makefile	Mon May 10 17:43:55 1999 +0200
@@ -5,7 +5,6 @@
 ## targets
 
 default: dvi
-dist: dvi
 
 
 ## dependencies
@@ -26,3 +25,15 @@
 	$(LATEX) $(NAME)
 	$(SEDINDEX) $(NAME)
 	$(LATEX) $(NAME)
+
+pdf: $(NAME).pdf
+
+$(NAME).pdf: $(FILES) isabelle_hol.pdf
+	touch $(NAME).ind
+	$(PDFLATEX) $(NAME)
+	$(BIBTEX) $(NAME)
+	$(PDFLATEX) $(NAME)
+	$(PDFLATEX) $(NAME)
+	$(SEDINDEX) $(NAME)
+	$(FIXBOOKMARKS) $(NAME).out
+	$(PDFLATEX) $(NAME)