# HG changeset patch
# User kleing
# Date 1052312015 -7200
# Node ID 9cdab3186c0bbd5ab82c2e891a61e957bd652797
# Parent  2160abf7cfe73ab8d04cfbd054b6a18758b334fe
fixed HOL-Real-HahnBanach (-> HOL-Complex-HahnBanach)

diff -r 2160abf7cfe7 -r 9cdab3186c0b src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Tue May 06 17:45:54 2003 +0200
+++ b/src/HOL/IsaMakefile	Wed May 07 14:53:35 2003 +0200
@@ -18,7 +18,7 @@
   HOL-Complex-ex \
   HOL-CTL \
   HOL-Extraction \
-      HOL-Real-HahnBanach \
+      HOL-Complex-HahnBanach \
   HOL-Hoare \
   HOL-HoareParallel \
   HOL-IMP \
@@ -113,11 +113,11 @@
 
 
 
-## HOL-Real-HahnBanach
+## HOL-Complex-HahnBanach
 
-HOL-Real-HahnBanach: HOL-Complex $(LOG)/HOL-Real-HahnBanach.gz
+HOL-Complex-HahnBanach: HOL-Complex $(LOG)/HOL-Complex-HahnBanach.gz
 
-$(LOG)/HOL-Real-HahnBanach.gz: $(OUT)/HOL-Real Real/HahnBanach/Aux.thy \
+$(LOG)/HOL-Complex-HahnBanach.gz: $(OUT)/HOL-Complex Real/HahnBanach/Aux.thy \
   Real/HahnBanach/Bounds.thy Real/HahnBanach/FunctionNorm.thy \
   Real/HahnBanach/FunctionOrder.thy Real/HahnBanach/HahnBanach.thy \
   Real/HahnBanach/HahnBanachExtLemmas.thy	\