diff -r 43ef6c6dd906 -r f88d0c363582 doc-src/TutorialI/IsaMakefile
--- a/doc-src/TutorialI/IsaMakefile	Fri Jul 05 11:47:44 2002 +0200
+++ b/doc-src/TutorialI/IsaMakefile	Fri Jul 05 17:48:05 2002 +0200
@@ -168,8 +168,8 @@
 HOL-Misc: HOL $(LOG)/HOL-Misc.gz
 
 $(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/Plus.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/appendix.thy
 	$(USEDIR) Misc
 	@rm -f tutorial.dvi