src/HOL/IsaMakefile
changeset 7535 599d3414b51d
parent 7513 879ae27f5e6f
child 7577 644f9b4ae764
     1.1 --- a/src/HOL/IsaMakefile	Thu Sep 09 19:01:37 1999 +0200
     1.2 +++ b/src/HOL/IsaMakefile	Fri Sep 10 17:28:51 1999 +0200
     1.3 @@ -12,7 +12,7 @@
     1.4    HOL-Auth HOL-UNITY HOL-Modelcheck HOL-Lambda HOL-W0 HOL-MiniML \
     1.5    HOL-IOA HOL-AxClasses-Group HOL-AxClasses-Lattice \
     1.6    HOL-AxClasses-Tutorial HOL-Quot HOL-ex HOL-Isar_examples HOL-Real-ex \
     1.7 -  TLA-Inc TLA-Buffer TLA-Memory
     1.8 +  HOL-Real-HahnBanach TLA-Inc TLA-Buffer TLA-Memory
     1.9  
    1.10  all: images test
    1.11  
    1.12 @@ -94,6 +94,21 @@
    1.13  	@cd Real; $(ISATOOL) usedir $(OUT)/HOL-Real ex
    1.14  
    1.15  
    1.16 +## HOL-Real-HahnBanach
    1.17 +
    1.18 +HOL-Real-HahnBanach: HOL-Real $(LOG)/HOL-Real-HahnBanach.gz
    1.19 +
    1.20 +$(LOG)/HOL-Real-HahnBanach.gz: $(OUT)/HOL-Real Real/HahnBanach/Aux.thy	\
    1.21 +  Real/HahnBanach/Bounds.thy Real/HahnBanach/FunctionNorm.thy		\
    1.22 +  Real/HahnBanach/FunctionOrder.thy Real/HahnBanach/HahnBanach.thy	\
    1.23 +  Real/HahnBanach/HahnBanach_h0_lemmas.thy				\
    1.24 +  Real/HahnBanach/HahnBanach_lemmas.thy					\
    1.25 +  Real/HahnBanach/LinearSpace.thy Real/HahnBanach/Linearform.thy	\
    1.26 +  Real/HahnBanach/NormedSpace.thy Real/HahnBanach/ROOT.ML		\
    1.27 +  Real/HahnBanach/Subspace.thy Real/HahnBanach/Zorn_Lemma.thy
    1.28 +	@cd Real; $(ISATOOL) usedir $(OUT)/HOL-Real HahnBanach
    1.29 +
    1.30 +
    1.31  ## HOL-Subst
    1.32  
    1.33  HOL-Subst: HOL $(LOG)/HOL-Subst.gz
    1.34 @@ -406,4 +421,5 @@
    1.35  	  $(LOG)/HOL-AxClasses-Tutorial.gz $(LOG)/HOL-Quot.gz \
    1.36  	  $(LOG)/HOL-ex.gz $(LOG)/HOL-Isar_examples.gz $(OUT)/TLA \
    1.37  	  $(LOG)/TLA.gz $(LOG)/TLA-Inc.gz $(LOG)/TLA-Buffer.gz \
    1.38 -	  $(LOG)/TLA-Memory.gz $(LOG)/HOL-Real-ex.gz
    1.39 +	  $(LOG)/TLA-Memory.gz $(LOG)/HOL-Real-ex.gz \
    1.40 +	  $(LOG)/HOL-Real-HahnBanach.gz