# HG changeset patch
# User paulson
# Date 978516831 -3600
# Node ID 94aa0b568009517ae1f44a5865e9f65f4fe444bb
# Parent  329d5f4aa43cc1098f63c4db52c9ccaf2bb58ee1
Types chapter now uses HOL-Real

diff -r 329d5f4aa43c -r 94aa0b568009 doc-src/TutorialI/IsaMakefile
--- a/doc-src/TutorialI/IsaMakefile	Wed Jan 03 11:13:13 2001 +0100
+++ b/doc-src/TutorialI/IsaMakefile	Wed Jan 03 11:13:51 2001 +0100
@@ -16,12 +16,16 @@
 OUT = $(ISABELLE_OUTPUT)
 LOG = $(OUT)/log
 USEDIR = @$(ISATOOL) usedir -m brackets -i true -d dvi -D document $(OUT)/HOL
+REALUSEDIR = @$(ISATOOL) usedir -m brackets -i true -d dvi -D document $(OUT)/HOL-Real
 
 ## HOL
 
 HOL:
 	@cd $(SRC)/HOL; $(ISATOOL) make HOL
 
+HOL-Real:
+	@cd $(SRC)/HOL; $(ISATOOL) make HOL-Real
+
 styles:
 	@rm -f isabelle.sty
 	@rm -f isabellesym.sty
@@ -145,13 +149,13 @@
 
 ## HOL-Types
 
-HOL-Types: HOL $(LOG)/HOL-Types.gz
+HOL-Types: HOL-Real $(LOG)/HOL-Types.gz
 
-$(LOG)/HOL-Types.gz: $(OUT)/HOL Types/ROOT.ML \
+$(LOG)/HOL-Types.gz: $(OUT)/HOL-Real Types/ROOT.ML \
   Types/Numbers.thy Types/Pairs.thy Types/Typedef.thy \
   Types/Overloading0.thy Types/Overloading1.thy Types/Overloading2.thy \
   Types/Overloading.thy Types/Axioms.thy
-	$(USEDIR) Types
+	$(REALUSEDIR) Types
 	@rm -f tutorial.dvi
 
 ## HOL-Misc