diff -r 193cf2fa692a -r 1bc0638d554d doc-src/Main/Makefile
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Main/Makefile	Wed Mar 11 12:51:00 2009 +0100
@@ -0,0 +1,45 @@
+#
+# $Id$
+#
+
+## targets
+
+default: dvi
+
+
+## dependencies
+
+include ../Makefile.in
+
+SRC = ../../src/HOL/Docs/generated
+
+NAME = main
+
+FILES = $(NAME).tex Main_Doc.tex \
+  isabelle.sty isabellesym.sty pdfsetup.sty
+
+dvi: $(NAME).dvi
+
+$(NAME).dvi: $(FILES)
+	$(LATEX) $(NAME)
+
+pdf: $(NAME).pdf
+
+$(NAME).pdf: $(FILES)
+	$(PDFLATEX) $(NAME)
+	$(FIXBOOKMARKS) $(NAME).out
+	$(PDFLATEX) $(NAME)
+	$(PDFLATEX) $(NAME)
+
+isabelle.sty:
+	ln ../isabelle.sty .
+
+isabellesym.sty:
+	ln ../isabellesym.sty .
+
+pdfsetup.sty:
+	ln ../pdfsetup.sty .
+
+copy:
+	cp $(SRC)/Main_Doc.tex Main_Doc.tex
+	cp $(SRC)/root.tex main.tex