1.1 --- a/doc-src/TutorialI/IsaMakefile	Fri Oct 13 11:15:56 2000 +0200
     1.2 +++ b/doc-src/TutorialI/IsaMakefile	Fri Oct 13 18:02:08 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-CTL HOL-Misc styles
     1.8 +default: HOL-ToyList HOL-Ifexpr HOL-CodeGen HOL-Trie HOL-Datatype HOL-Recdef HOL-Advanced HOL-CTL HOL-Inductive HOL-Misc styles
     1.9  images:
    1.10  test:
    1.11  all: default
    1.12 @@ -110,6 +110,14 @@
    1.13  	@$(ISATOOL) usedir -i true -d dvi -D document $(OUT)/HOL CTL
    1.14  	@rm -f tutorial.dvi
    1.15  
    1.16 +## HOL-Inductive
    1.17 +
    1.18 +HOL-Inductive: HOL $(LOG)/HOL-Inductive.gz
    1.19 +
    1.20 +$(LOG)/HOL-Inductive.gz: $(OUT)/HOL Inductive/AB.thy Inductive/ROOT.ML
    1.21 +	@$(ISATOOL) usedir -i true -d dvi -D document $(OUT)/HOL Inductive
    1.22 +	@rm -f tutorial.dvi
    1.23 +
    1.24  ## HOL-Misc
    1.25  
    1.26  HOL-Misc: HOL $(LOG)/HOL-Misc.gz
    1.27 @@ -126,4 +134,4 @@
    1.28  ## clean
    1.29  
    1.30  clean:
    1.31 -	@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-CTL.gz
    1.32 +	@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-CTL.gz $(LOG)/HOL-Inductive.gz