diff -r 6a7d80a139c6 -r 0538cb0f7999 doc-src/TutorialI/Makefile
--- a/doc-src/TutorialI/Makefile	Mon Oct 01 14:42:47 2001 +0200
+++ b/doc-src/TutorialI/Makefile	Mon Oct 01 14:44:00 2001 +0200
@@ -22,6 +22,7 @@
 	Protocol/protocol.tex \
 	Rules/rules.tex Sets/sets.tex \
 	Types/numerics.tex Types/records.tex Types/types.tex \
+	Documents/documents.tex \
 	../iman.sty ../ttbox.sty ../extra.sty \
 	isabelle.sty isabellesym.sty ../pdfsetup.sty