diff -r becd902a0e97 -r 08dfd050b373 doc-src/Intro/Makefile
--- a/doc-src/Intro/Makefile	Thu May 06 18:48:46 1999 +0200
+++ b/doc-src/Intro/Makefile	Thu May 06 19:04:20 1999 +0200
@@ -26,3 +26,16 @@
 	$(LATEX) $(NAME)
 	$(SEDINDEX) $(NAME)
 	$(LATEX) $(NAME)
+
+
+pdf: $(NAME).pdf
+
+$(NAME).pdf: $(FILES) isabelle.png
+	touch $(NAME).ind
+	$(PDFLATEX) $(NAME)
+	$(BIBTEX) $(NAME)
+	$(PDFLATEX) $(NAME)
+	$(PDFLATEX) $(NAME)
+	$(SEDINDEX) $(NAME)
+	$(FIXBOOKMARKS) $(NAME).out
+	$(PDFLATEX) $(NAME)