src/HOL/IsaMakefile
changeset 7917 5e5b9813cce7
parent 7799 4c69318e6a6d
child 7926 9c20924de52c
     1.1 --- a/src/HOL/IsaMakefile	Fri Oct 22 18:41:00 1999 +0200
     1.2 +++ b/src/HOL/IsaMakefile	Fri Oct 22 20:14:31 1999 +0200
     1.3 @@ -101,12 +101,12 @@
     1.4  $(LOG)/HOL-Real-HahnBanach.gz: $(OUT)/HOL-Real Real/HahnBanach/Aux.thy \
     1.5    Real/HahnBanach/Bounds.thy Real/HahnBanach/FunctionNorm.thy \
     1.6    Real/HahnBanach/FunctionOrder.thy Real/HahnBanach/HahnBanach.thy \
     1.7 -  Real/HahnBanach/HahnBanach_h0_lemmas.thy	\
     1.8 -  Real/HahnBanach/HahnBanach_lemmas.thy		\
     1.9 -  Real/HahnBanach/LinearSpace.thy Real/HahnBanach/Linearform.thy \
    1.10 -  Real/HahnBanach/NormedSpace.thy Real/HahnBanach/ROOT.ML \
    1.11 -  Real/HahnBanach/Subspace.thy Real/HahnBanach/Zorn_Lemma.thy \
    1.12 -  Real/HahnBanach/document/notation.tex		\
    1.13 +  Real/HahnBanach/HahnBanachExtLemmas.thy	\
    1.14 +  Real/HahnBanach/HahnBanachSupLemmas.thy	\
    1.15 +  Real/HahnBanach/Linearform.thy Real/HahnBanach/NormedSpace.thy \
    1.16 +  Real/HahnBanach/README.html Real/HahnBanach/ROOT.ML \
    1.17 +  Real/HahnBanach/Subspace.thy Real/HahnBanach/VectorSpace.thy \
    1.18 +  Real/HahnBanach/ZornLemma.thy Real/HahnBanach/document/notation.tex \
    1.19    Real/HahnBanach/document/root.tex
    1.20  	@cd Real; $(ISATOOL) usedir $(OUT)/HOL-Real HahnBanach
    1.21