include document;
authorwenzelm
Fri Oct 08 15:08:47 1999 +0200 (1999-10-08)
changeset 77994c69318e6a6d
parent 7798 42e94b618f34
child 7800 8ee919e42174
include document;
src/HOL/IsaMakefile
     1.1 --- a/src/HOL/IsaMakefile	Fri Oct 08 15:08:23 1999 +0200
     1.2 +++ b/src/HOL/IsaMakefile	Fri Oct 08 15:08:47 1999 +0200
     1.3 @@ -98,14 +98,16 @@
     1.4  
     1.5  HOL-Real-HahnBanach: HOL-Real $(LOG)/HOL-Real-HahnBanach.gz
     1.6  
     1.7 -$(LOG)/HOL-Real-HahnBanach.gz: $(OUT)/HOL-Real Real/HahnBanach/Aux.thy	\
     1.8 -  Real/HahnBanach/Bounds.thy Real/HahnBanach/FunctionNorm.thy		\
     1.9 -  Real/HahnBanach/FunctionOrder.thy Real/HahnBanach/HahnBanach.thy	\
    1.10 -  Real/HahnBanach/HahnBanach_h0_lemmas.thy				\
    1.11 -  Real/HahnBanach/HahnBanach_lemmas.thy					\
    1.12 -  Real/HahnBanach/LinearSpace.thy Real/HahnBanach/Linearform.thy	\
    1.13 -  Real/HahnBanach/NormedSpace.thy Real/HahnBanach/ROOT.ML		\
    1.14 -  Real/HahnBanach/Subspace.thy Real/HahnBanach/Zorn_Lemma.thy
    1.15 +$(LOG)/HOL-Real-HahnBanach.gz: $(OUT)/HOL-Real Real/HahnBanach/Aux.thy \
    1.16 +  Real/HahnBanach/Bounds.thy Real/HahnBanach/FunctionNorm.thy \
    1.17 +  Real/HahnBanach/FunctionOrder.thy Real/HahnBanach/HahnBanach.thy \
    1.18 +  Real/HahnBanach/HahnBanach_h0_lemmas.thy	\
    1.19 +  Real/HahnBanach/HahnBanach_lemmas.thy		\
    1.20 +  Real/HahnBanach/LinearSpace.thy Real/HahnBanach/Linearform.thy \
    1.21 +  Real/HahnBanach/NormedSpace.thy Real/HahnBanach/ROOT.ML \
    1.22 +  Real/HahnBanach/Subspace.thy Real/HahnBanach/Zorn_Lemma.thy \
    1.23 +  Real/HahnBanach/document/notation.tex		\
    1.24 +  Real/HahnBanach/document/root.tex
    1.25  	@cd Real; $(ISATOOL) usedir $(OUT)/HOL-Real HahnBanach
    1.26  
    1.27  
    1.28 @@ -372,7 +374,8 @@
    1.29    Isar_examples/KnasterTarski.thy Isar_examples/MultisetOrder.thy \
    1.30    Isar_examples/MutilatedCheckerboard.thy Isar_examples/Peirce.thy \
    1.31    Isar_examples/Summation.thy Isar_examples/ROOT.ML \
    1.32 -  Isar_examples/W_correct.thy
    1.33 +  Isar_examples/W_correct.thy Isar_examples/document/root.tex \
    1.34 +  Isar_examples/document/style.tex
    1.35  	@$(ISATOOL) usedir $(OUT)/HOL Isar_examples
    1.36  
    1.37