src/HOL/IsaMakefile
changeset 13967 9cdab3186c0b
parent 13966 2160abf7cfe7
child 13980 f254d1c92a6a
     1.1 --- a/src/HOL/IsaMakefile	Tue May 06 17:45:54 2003 +0200
     1.2 +++ b/src/HOL/IsaMakefile	Wed May 07 14:53:35 2003 +0200
     1.3 @@ -18,7 +18,7 @@
     1.4    HOL-Complex-ex \
     1.5    HOL-CTL \
     1.6    HOL-Extraction \
     1.7 -      HOL-Real-HahnBanach \
     1.8 +      HOL-Complex-HahnBanach \
     1.9    HOL-Hoare \
    1.10    HOL-HoareParallel \
    1.11    HOL-IMP \
    1.12 @@ -113,11 +113,11 @@
    1.13  
    1.14  
    1.15  
    1.16 -## HOL-Real-HahnBanach
    1.17 +## HOL-Complex-HahnBanach
    1.18  
    1.19 -HOL-Real-HahnBanach: HOL-Complex $(LOG)/HOL-Real-HahnBanach.gz
    1.20 +HOL-Complex-HahnBanach: HOL-Complex $(LOG)/HOL-Complex-HahnBanach.gz
    1.21  
    1.22 -$(LOG)/HOL-Real-HahnBanach.gz: $(OUT)/HOL-Real Real/HahnBanach/Aux.thy \
    1.23 +$(LOG)/HOL-Complex-HahnBanach.gz: $(OUT)/HOL-Complex Real/HahnBanach/Aux.thy \
    1.24    Real/HahnBanach/Bounds.thy Real/HahnBanach/FunctionNorm.thy \
    1.25    Real/HahnBanach/FunctionOrder.thy Real/HahnBanach/HahnBanach.thy \
    1.26    Real/HahnBanach/HahnBanachExtLemmas.thy	\