# HG changeset patch
# User wenzelm
# Date 926010260 -7200
# Node ID 08dfd050b3731421839cfca8e47cf73384c8090b
# Parent  becd902a0e97d4c3090ea5fc7448f8b21cc72a1f
pdf setup;

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)
diff -r becd902a0e97 -r 08dfd050b373 doc-src/Intro/intro.tex
--- a/doc-src/Intro/intro.tex	Thu May 06 18:48:46 1999 +0200
+++ b/doc-src/Intro/intro.tex	Thu May 06 19:04:20 1999 +0200
@@ -7,7 +7,7 @@
 %prth *(\(.*\));          \1;      
 %{\\out \(.*\)}          {\\out val it = "\1" : thm}
 
-\title{\includegraphics[scale=0.5]{isabelle.eps} \\[4ex] Introduction to Isabelle}   
+\title{\includegraphics[scale=0.5]{isabelle} \\[4ex] Introduction to Isabelle}   
 \author{{\em Lawrence C. Paulson}\\
         Computer Laboratory \\ University of Cambridge \\
         \texttt{lcp@cl.cam.ac.uk}\\[3ex]