diff -r a4772a650b4e -r a7a30ba65d0a src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Mon Mar 09 22:43:25 2009 +0100
+++ b/src/HOL/IsaMakefile	Mon Mar 09 22:56:39 2009 +0100
@@ -15,6 +15,7 @@
   HOL-Auth \
   HOL-Bali \
   HOL-Decision_Procs \
+  HOL-Docs \
   HOL-Extraction \
   HOL-HahnBanach \
   HOL-Hoare \
@@ -683,6 +684,15 @@
 	@$(ISABELLE_TOOL) usedir $(OUT)/HOL Decision_Procs
 
 
+## HOL-Docs
+
+HOL-Docs: HOL $(LOG)/HOL-Docs.gz
+
+$(LOG)/HOL-Docs.gz: $(OUT)/HOL Docs/Main_Doc.thy Docs/ROOT.ML	\
+  Docs/document/root.tex
+	@$(ISABELLE_TOOL) usedir $(OUT)/HOL Docs
+
+
 ## HOL-Lambda
 
 HOL-Lambda: HOL $(LOG)/HOL-Lambda.gz