diff -r 19214ac381cf -r bf33cbd76c05 doc-src/TutorialI/IsaMakefile
--- a/doc-src/TutorialI/IsaMakefile	Wed Oct 25 17:44:59 2000 +0200
+++ b/doc-src/TutorialI/IsaMakefile	Wed Oct 25 18:24:33 2000 +0200
@@ -4,7 +4,7 @@
 
 ## targets
 
-default: HOL-ToyList HOL-Ifexpr HOL-CodeGen HOL-Trie HOL-Datatype HOL-Recdef HOL-Advanced HOL-Rules HOL-Sets HOL-CTL HOL-Inductive HOL-Misc styles
+default: HOL-ToyList HOL-Ifexpr HOL-CodeGen HOL-Trie HOL-Datatype HOL-Recdef HOL-Advanced HOL-Rules HOL-Sets HOL-CTL HOL-Inductive  HOL-Types HOL-Misc styles
 images:
 test:
 all: default
@@ -138,6 +138,16 @@
 	@$(ISATOOL) usedir -i true -d dvi -D document $(OUT)/HOL Inductive
 	@rm -f tutorial.dvi
 
+## HOL-Types
+
+HOL-Types: HOL $(LOG)/HOL-Types.gz
+
+$(LOG)/HOL-Types.gz: $(OUT)/HOL Types/ROOT.ML \
+  Types/Overloading0.thy Types/Overloading1.thy Types/Overloading2.thy \
+  Types/Overloading.thy Types/Axioms.thy
+	@$(ISATOOL) usedir -i true -d dvi -D document $(OUT)/HOL Types
+	@rm -f tutorial.dvi
+
 ## HOL-Misc
 
 HOL-Misc: HOL $(LOG)/HOL-Misc.gz
@@ -154,4 +164,4 @@
 ## clean
 
 clean:
-	@rm -f tutorial.dvi $(LOG)/HOL-Ifexpr.gz $(LOG)/HOL-CodeGen.gz $(LOG)/HOL-Misc.gz $(LOG)/HOL-ToyList.gz $(LOG)/HOL-ToyList2.gz $(LOG)/HOL-Trie.gz $(LOG)/HOL-Datatype.gz $(LOG)/HOL-Recdef.gz $(LOG)/HOL-Advanced.gz $(LOG)/HOL-Rules.gz $(LOG)/HOL-Sets.gz $(LOG)/HOL-CTL.gz $(LOG)/HOL-Inductive.gz
+	@rm -f tutorial.dvi $(LOG)/HOL-Ifexpr.gz $(LOG)/HOL-CodeGen.gz $(LOG)/HOL-Misc.gz $(LOG)/HOL-ToyList.gz $(LOG)/HOL-ToyList2.gz $(LOG)/HOL-Trie.gz $(LOG)/HOL-Datatype.gz $(LOG)/HOL-Recdef.gz $(LOG)/HOL-Advanced.gz $(LOG)/HOL-Rules.gz $(LOG)/HOL-Sets.gz $(LOG)/HOL-CTL.gz $(LOG)/HOL-Inductive.gz $(LOG)/HOL-Types.gz