1.1 --- a/doc-src/TutorialI/IsaMakefile	Thu May 08 10:35:24 2003 +0200
     1.2 +++ b/doc-src/TutorialI/IsaMakefile	Thu May 08 12:50:27 2003 +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-Recdef \
     1.7 -  HOL-Advanced HOL-Rules HOL-Sets HOL-CTL HOL-Inductive  HOL-Real-Types HOL-Misc \
     1.8 +  HOL-Advanced HOL-Rules HOL-Sets HOL-CTL HOL-Inductive  HOL-Complex-Types HOL-Misc \
     1.9    HOL-Protocol HOL-Documents styles
    1.10  images:
    1.11  test:
    1.12 @@ -19,7 +19,7 @@
    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-Real
    1.17 +REALUSEDIR = @$(ISATOOL) usedir $(OPTIONS) $(OUT)/HOL-Complex
    1.18  
    1.19  
    1.20  ## HOL
    1.21 @@ -27,8 +27,8 @@
    1.22  HOL:
    1.23  	@cd $(SRC)/HOL; $(ISATOOL) make HOL
    1.24  
    1.25 -HOL-Real:
    1.26 -	@cd $(SRC)/HOL; $(ISATOOL) make HOL-Real
    1.27 +HOL-Complex:
    1.28 +	@cd $(SRC)/HOL; $(ISATOOL) make HOL-Complex
    1.29  
    1.30  styles:
    1.31  	@rm -f isabelle.sty
    1.32 @@ -154,9 +154,9 @@
    1.33  
    1.34  ## HOL-Types
    1.35  
    1.36 -HOL-Real-Types: HOL-Real $(LOG)/HOL-Real-Types.gz
    1.37 +HOL-Complex-Types: HOL-Complex $(LOG)/HOL-Complex-Types.gz
    1.38  
    1.39 -$(LOG)/HOL-Real-Types.gz: $(OUT)/HOL-Real Types/ROOT.ML \
    1.40 +$(LOG)/HOL-Complex-Types.gz: $(OUT)/HOL-Complex Types/ROOT.ML \
    1.41    Types/Numbers.thy Types/Pairs.thy Types/Records.thy Types/Typedefs.thy \
    1.42    Types/Overloading0.thy Types/Overloading1.thy Types/Overloading2.thy \
    1.43    Types/Overloading.thy Types/Axioms.thy