src/HOL/IsaMakefile
changeset 13967 9cdab3186c0b
parent 13966 2160abf7cfe7
child 13980 f254d1c92a6a
--- 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	\