# HG changeset patch
# User nipkow
# Date 978705574 -3600
# Node ID 778f0897e7e5612d4cb4d2d29706c42d4f4940ad
# Parent  520dd8696927da6ff34fc3063719eba05add45c0
*** empty log message ***

diff -r 520dd8696927 -r 778f0897e7e5 doc-src/TutorialI/IsaMakefile
--- a/doc-src/TutorialI/IsaMakefile	Fri Jan 05 15:16:40 2001 +0100
+++ b/doc-src/TutorialI/IsaMakefile	Fri Jan 05 15:39:34 2001 +0100
@@ -4,7 +4,7 @@
 
 ## targets
 
-default: HOL-ToyList HOL-Ifexpr HOL-CodeGen HOL-Trie HOL-Datatype HOL-Recdef HOL-Advanced HOL-Rules HOL-Sets HOL-CTL HOL-Inductive  HOL-Types HOL-Misc styles
+default: HOL-ToyList HOL-Ifexpr HOL-CodeGen HOL-Trie HOL-Datatype HOL-Recdef HOL-Advanced HOL-Rules HOL-Sets HOL-CTL HOL-Inductive  HOL-Real-Types HOL-Misc styles
 images:
 test:
 all: default
@@ -149,9 +149,9 @@
 
 ## HOL-Types
 
-HOL-Types: HOL-Real $(LOG)/HOL-Types.gz
+HOL-Real-Types: HOL-Real $(LOG)/HOL-Real-Types.gz
 
-$(LOG)/HOL-Types.gz: $(OUT)/HOL-Real Types/ROOT.ML \
+$(LOG)/HOL-Real-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