diff -r 8a5b3f58b944 -r 3253c6046d57 doc-src/TutorialI/Makefile
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/TutorialI/Makefile	Wed Apr 19 11:54:39 2000 +0200
@@ -0,0 +1,39 @@
+#
+# $Id$
+#
+
+## targets
+
+default: dvi
+
+
+## dependencies
+
+include ../Makefile.in
+
+NAME = tutorial
+FILES = tutorial.tex basics.tex fp.tex appendix.tex \
+	../iman.sty ttbox.sty extra.sty
+
+dvi: $(NAME).dvi
+
+$(NAME).dvi: $(FILES) isabelle_hol.eps
+	touch $(NAME).ind
+	$(LATEX) $(NAME)
+	$(BIBTEX) $(NAME)
+	$(LATEX) $(NAME)
+	$(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)