# HG changeset patch
# User haftmann
# Date 1214892308 -7200
# Node ID b8ff8497de6aa48fce0b092c563e280b2dfe4fb4
# Parent  73d25d42212416d7070766ae5d6aaa97de920e36
HOL += HOL-Complex

diff -r 73d25d422124 -r b8ff8497de6a doc-src/TutorialI/IsaMakefile
--- a/doc-src/TutorialI/IsaMakefile	Tue Jul 01 07:58:37 2008 +0200
+++ b/doc-src/TutorialI/IsaMakefile	Tue Jul 01 08:05:08 2008 +0200
@@ -5,7 +5,7 @@
 ## targets
 
 default: HOL-ToyList HOL-Ifexpr HOL-CodeGen HOL-Trie HOL-Datatype HOL-Fun HOL-Fun \
-  HOL-Advanced HOL-Rules HOL-Sets HOL-CTL HOL-Inductive  HOL-Complex-Types HOL-Misc \
+  HOL-Advanced HOL-Rules HOL-Sets HOL-CTL HOL-Inductive  HOL-Types HOL-Misc \
   HOL-Protocol HOL-Documents styles
 images:
 test:
@@ -19,7 +19,6 @@
 LOG = $(OUT)/log
 OPTIONS = -m brackets -i true -d "" -D document
 USEDIR = @$(ISATOOL) usedir $(OPTIONS) $(OUT)/HOL
-REALUSEDIR = @$(ISATOOL) usedir $(OPTIONS) $(OUT)/HOL-Complex
 
 
 ## HOL
@@ -27,9 +26,6 @@
 HOL:
 	@cd $(SRC)/HOL; $(ISATOOL) make HOL
 
-HOL-Complex:
-	@cd $(SRC)/HOL; $(ISATOOL) make HOL-Complex
-
 styles:
 	@rm -f isabelle.sty
 	@rm -f isabellesym.sty
@@ -151,13 +147,13 @@
 
 ## HOL-Types
 
-HOL-Complex-Types: HOL-Complex $(LOG)/HOL-Complex-Types.gz
+HOL-Types: HOL $(LOG)/HOL-Types.gz
 
-$(LOG)/HOL-Complex-Types.gz: $(OUT)/HOL-Complex Types/ROOT.ML \
+$(LOG)/HOL-Types.gz: $(OUT)/HOL Types/ROOT.ML \
   Types/Numbers.thy Types/Pairs.thy Types/Records.thy Types/Typedefs.thy \
   Types/Overloading0.thy Types/Overloading1.thy Types/Overloading2.thy \
   Types/Overloading.thy Types/Axioms.thy
-	$(REALUSEDIR) Types
+	$(USEDIR) Types
 	@rm -f tutorial.dvi
 
 ## HOL-Misc