1.1 --- a/doc-src/TutorialI/IsaMakefile	Tue Jul 01 07:58:37 2008 +0200
     1.2 +++ b/doc-src/TutorialI/IsaMakefile	Tue Jul 01 08:05:08 2008 +0200
     1.3 @@ -5,7 +5,7 @@
     1.4  ## targets
     1.5  
     1.6  default: HOL-ToyList HOL-Ifexpr HOL-CodeGen HOL-Trie HOL-Datatype HOL-Fun HOL-Fun \
     1.7 -  HOL-Advanced HOL-Rules HOL-Sets HOL-CTL HOL-Inductive  HOL-Complex-Types HOL-Misc \
     1.8 +  HOL-Advanced HOL-Rules HOL-Sets HOL-CTL HOL-Inductive  HOL-Types HOL-Misc \
     1.9    HOL-Protocol HOL-Documents styles
    1.10  images:
    1.11  test:
    1.12 @@ -19,7 +19,6 @@
    1.13  LOG = $(OUT)/log
    1.14  OPTIONS = -m brackets -i true -d "" -D document
    1.15  USEDIR = @$(ISATOOL) usedir $(OPTIONS) $(OUT)/HOL
    1.16 -REALUSEDIR = @$(ISATOOL) usedir $(OPTIONS) $(OUT)/HOL-Complex
    1.17  
    1.18  
    1.19  ## HOL
    1.20 @@ -27,9 +26,6 @@
    1.21  HOL:
    1.22  	@cd $(SRC)/HOL; $(ISATOOL) make HOL
    1.23  
    1.24 -HOL-Complex:
    1.25 -	@cd $(SRC)/HOL; $(ISATOOL) make HOL-Complex
    1.26 -
    1.27  styles:
    1.28  	@rm -f isabelle.sty
    1.29  	@rm -f isabellesym.sty
    1.30 @@ -151,13 +147,13 @@
    1.31  
    1.32  ## HOL-Types
    1.33  
    1.34 -HOL-Complex-Types: HOL-Complex $(LOG)/HOL-Complex-Types.gz
    1.35 +HOL-Types: HOL $(LOG)/HOL-Types.gz
    1.36  
    1.37 -$(LOG)/HOL-Complex-Types.gz: $(OUT)/HOL-Complex Types/ROOT.ML \
    1.38 +$(LOG)/HOL-Types.gz: $(OUT)/HOL Types/ROOT.ML \
    1.39    Types/Numbers.thy Types/Pairs.thy Types/Records.thy Types/Typedefs.thy \
    1.40    Types/Overloading0.thy Types/Overloading1.thy Types/Overloading2.thy \
    1.41    Types/Overloading.thy Types/Axioms.thy
    1.42 -	$(REALUSEDIR) Types
    1.43 +	$(USEDIR) Types
    1.44  	@rm -f tutorial.dvi
    1.45  
    1.46  ## HOL-Misc