fixed HOL-Real-HahnBanach (-> HOL-Complex-HahnBanach)
authorkleing
Wed, 07 May 2003 14:53:35 +0200
changeset 13967 9cdab3186c0b
parent 13966 2160abf7cfe7
child 13968 689868b99bde
fixed HOL-Real-HahnBanach (-> HOL-Complex-HahnBanach)
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	\