diff -r 07ec657249e5 -r 90b0fc84f8d9 src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Sun Dec 09 14:35:36 2001 +0100
+++ b/src/HOL/IsaMakefile	Sun Dec 09 14:36:14 2001 +0100
@@ -226,10 +226,11 @@
 
 HOL-IMP: HOL $(LOG)/HOL-IMP.gz
 
-$(LOG)/HOL-IMP.gz: $(OUT)/HOL IMP/Com.thy IMP/Compiler.thy IMP/Denotation.ML \
-  IMP/Denotation.thy IMP/Expr.ML IMP/Expr.thy IMP/Hoare.ML IMP/Hoare.thy \
-  IMP/Natural.ML IMP/Natural.thy IMP/Examples.ML IMP/Examples.thy \
-  IMP/Transition.ML IMP/Transition.thy IMP/VC.ML IMP/VC.thy IMP/ROOT.ML
+$(LOG)/HOL-IMP.gz: $(OUT)/HOL IMP/Com.thy IMP/Compiler.thy \
+  IMP/Denotation.thy IMP/Expr.thy IMP/Hoare.thy \
+  IMP/Natural.thy IMP/Examples.thy \
+  IMP/Transition.thy IMP/VC.thy IMP/ROOT.ML IMP/document/root.tex \
+  IMP/document/root.bib
 	@$(ISATOOL) usedir $(OUT)/HOL IMP