1.1 --- a/doc-src/TutorialI/IsaMakefile	Wed Oct 25 17:44:59 2000 +0200
     1.2 +++ b/doc-src/TutorialI/IsaMakefile	Wed Oct 25 18:24:33 2000 +0200
     1.3 @@ -4,7 +4,7 @@
     1.4  
     1.5  ## targets
     1.6  
     1.7 -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
     1.8 +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
     1.9  images:
    1.10  test:
    1.11  all: default
    1.12 @@ -138,6 +138,16 @@
    1.13  	@$(ISATOOL) usedir -i true -d dvi -D document $(OUT)/HOL Inductive
    1.14  	@rm -f tutorial.dvi
    1.15  
    1.16 +## HOL-Types
    1.17 +
    1.18 +HOL-Types: HOL $(LOG)/HOL-Types.gz
    1.19 +
    1.20 +$(LOG)/HOL-Types.gz: $(OUT)/HOL Types/ROOT.ML \
    1.21 +  Types/Overloading0.thy Types/Overloading1.thy Types/Overloading2.thy \
    1.22 +  Types/Overloading.thy Types/Axioms.thy
    1.23 +	@$(ISATOOL) usedir -i true -d dvi -D document $(OUT)/HOL Types
    1.24 +	@rm -f tutorial.dvi
    1.25 +
    1.26  ## HOL-Misc
    1.27  
    1.28  HOL-Misc: HOL $(LOG)/HOL-Misc.gz
    1.29 @@ -154,4 +164,4 @@
    1.30  ## clean
    1.31  
    1.32  clean:
    1.33 -	@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
    1.34 +	@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