diff -r 4b47d8aaf5af -r 5eebea8f359f doc-src/TutorialI/IsaMakefile
--- a/doc-src/TutorialI/IsaMakefile	Thu Jan 25 11:59:52 2001 +0100
+++ b/doc-src/TutorialI/IsaMakefile	Thu Jan 25 15:31:31 2001 +0100
@@ -165,7 +165,7 @@
 $(LOG)/HOL-Misc.gz: $(OUT)/HOL Misc/ROOT.ML Misc/Tree.thy Misc/Tree2.thy \
   Misc/fakenat.thy Misc/natsum.thy Misc/pairs.thy Misc/Option2.thy \
   Misc/types.thy Misc/prime_def.thy Misc/case_exprs.thy \
-  Misc/simp.thy Misc/Itrev.thy Misc/AdvancedInd.thy
+  Misc/simp.thy Misc/Itrev.thy Misc/AdvancedInd.thy Misc/appendix.thy
 	$(USEDIR) Misc
 	@rm -f tutorial.dvi