src/HOL/IsaMakefile
changeset 31795 be3e1cc5005c
parent 31771 1a92eb45060f
child 31807 039893a9a77d
     1.1 --- a/src/HOL/IsaMakefile	Wed Jun 24 21:28:02 2009 +0200
     1.2 +++ b/src/HOL/IsaMakefile	Wed Jun 24 21:46:54 2009 +0200
     1.3 @@ -16,7 +16,7 @@
     1.4    HOL-Bali \
     1.5    HOL-Decision_Procs \
     1.6    HOL-Extraction \
     1.7 -  HOL-HahnBanach \
     1.8 +  HOL-Hahn_Banach \
     1.9    HOL-Hoare \
    1.10    HOL-HoareParallel \
    1.11    HOL-Import \
    1.12 @@ -360,21 +360,19 @@
    1.13  	@cd Library; $(ISABELLE_TOOL) usedir $(OUT)/HOL Library
    1.14  
    1.15  
    1.16 -## HOL-HahnBanach
    1.17 +## HOL-Hahn_Banach
    1.18  
    1.19 -HOL-HahnBanach: HOL $(LOG)/HOL-HahnBanach.gz
    1.20 +HOL-Hahn_Banach: HOL $(LOG)/HOL-Hahn_Banach.gz
    1.21  
    1.22 -$(LOG)/HOL-HahnBanach.gz: $(OUT)/HOL			\
    1.23 -  HahnBanach/Bounds.thy HahnBanach/FunctionNorm.thy		\
    1.24 -  HahnBanach/FunctionOrder.thy HahnBanach/HahnBanach.thy	\
    1.25 -  HahnBanach/HahnBanachExtLemmas.thy				\
    1.26 -  HahnBanach/HahnBanachSupLemmas.thy				\
    1.27 -  HahnBanach/Linearform.thy HahnBanach/NormedSpace.thy	\
    1.28 -  HahnBanach/README.html HahnBanach/ROOT.ML			\
    1.29 -  HahnBanach/Subspace.thy HahnBanach/VectorSpace.thy		\
    1.30 -  HahnBanach/ZornLemma.thy HahnBanach/document/root.bib	\
    1.31 -  HahnBanach/document/root.tex
    1.32 -	@$(ISABELLE_TOOL) usedir -g true $(OUT)/HOL HahnBanach
    1.33 +$(LOG)/HOL-Hahn_Banach.gz: $(OUT)/HOL Hahn_Banach/Bounds.thy		\
    1.34 +  Hahn_Banach/Function_Norm.thy Hahn_Banach/Function_Order.thy		\
    1.35 +  Hahn_Banach/Hahn_Banach.thy Hahn_Banach/Hahn_Banach_Ext_Lemmas.thy	\
    1.36 +  Hahn_Banach/Hahn_Banach_Sup_Lemmas.thy Hahn_Banach/Linearform.thy	\
    1.37 +  Hahn_Banach/Normed_Space.thy Hahn_Banach/README.html			\
    1.38 +  Hahn_Banach/ROOT.ML Hahn_Banach/Subspace.thy				\
    1.39 +  Hahn_Banach/Vector_Space.thy Hahn_Banach/Zorn_Lemma.thy		\
    1.40 +  Hahn_Banach/document/root.bib Hahn_Banach/document/root.tex
    1.41 +	@$(ISABELLE_TOOL) usedir -g true $(OUT)/HOL Hahn_Banach
    1.42  
    1.43  
    1.44  ## HOL-Subst
    1.45 @@ -1138,7 +1136,7 @@
    1.46  		$(LOG)/HOL-MicroJava.gz $(LOG)/HOL-NanoJava.gz		\
    1.47  		$(LOG)/HOL-Nominal-Examples.gz $(LOG)/HOL-IOA.gz	\
    1.48  		$(LOG)/HOL-Lattice $(LOG)/HOL-Matrix			\
    1.49 -		$(LOG)/HOL-HahnBanach.gz $(LOG)/HOL-SET-Protocol.gz	\
    1.50 +		$(LOG)/HOL-Hahn_Banach.gz $(LOG)/HOL-SET-Protocol.gz	\
    1.51  		$(LOG)/TLA-Inc.gz $(LOG)/TLA-Buffer.gz			\
    1.52  		$(LOG)/TLA-Memory.gz $(LOG)/HOL-Library.gz		\
    1.53  		$(LOG)/HOL-Unix.gz $(OUT)/HOL-Word $(LOG)/HOL-Word.gz	\