src/HOL/IsaMakefile
changeset 29197 6d4cb27ed19c
parent 29181 cc177742e607
child 29399 ebcd69a00872
     1.1 --- a/src/HOL/IsaMakefile	Mon Dec 29 13:23:53 2008 +0100
     1.2 +++ b/src/HOL/IsaMakefile	Mon Dec 29 14:08:08 2008 +0100
     1.3 @@ -261,7 +261,7 @@
     1.4  $(OUT)/HOL: ROOT.ML $(MAIN_DEPENDENCIES) \
     1.5    Complex_Main.thy \
     1.6    Complex.thy \
     1.7 -  Complex/Fundamental_Theorem_Algebra.thy \
     1.8 +  Fundamental_Theorem_Algebra.thy \
     1.9    Deriv.thy \
    1.10    Fact.thy \
    1.11    FrechetDeriv.thy \
    1.12 @@ -271,11 +271,11 @@
    1.13    Log.thy \
    1.14    MacLaurin.thy \
    1.15    NthRoot.thy \
    1.16 -  Hyperreal/SEQ.thy \
    1.17 +  SEQ.thy \
    1.18    Series.thy \
    1.19    Taylor.thy \
    1.20    Transcendental.thy \
    1.21 -  Library/Dense_Linear_Order.thy \
    1.22 +  Dense_Linear_Order.thy \
    1.23    GCD.thy \
    1.24    Order_Relation.thy \
    1.25    Parity.thy \
    1.26 @@ -287,7 +287,7 @@
    1.27    RealDef.thy \
    1.28    RealPow.thy \
    1.29    Real.thy \
    1.30 -  Real/RealVector.thy \
    1.31 +  RealVector.thy \
    1.32    Tools/float_syntax.ML \
    1.33    Tools/rat_arith.ML \
    1.34    Tools/real_arith.ML \
    1.35 @@ -337,16 +337,16 @@
    1.36  HOL-HahnBanach: HOL $(LOG)/HOL-HahnBanach.gz
    1.37  
    1.38  $(LOG)/HOL-HahnBanach.gz: $(OUT)/HOL			\
    1.39 -  Real/HahnBanach/Bounds.thy Real/HahnBanach/FunctionNorm.thy		\
    1.40 -  Real/HahnBanach/FunctionOrder.thy Real/HahnBanach/HahnBanach.thy	\
    1.41 -  Real/HahnBanach/HahnBanachExtLemmas.thy				\
    1.42 -  Real/HahnBanach/HahnBanachSupLemmas.thy				\
    1.43 -  Real/HahnBanach/Linearform.thy Real/HahnBanach/NormedSpace.thy	\
    1.44 -  Real/HahnBanach/README.html Real/HahnBanach/ROOT.ML			\
    1.45 -  Real/HahnBanach/Subspace.thy Real/HahnBanach/VectorSpace.thy		\
    1.46 -  Real/HahnBanach/ZornLemma.thy Real/HahnBanach/document/root.bib	\
    1.47 -  Real/HahnBanach/document/root.tex
    1.48 -	@cd Real; $(ISABELLE_TOOL) usedir -g true $(OUT)/HOL HahnBanach
    1.49 +  HahnBanach/Bounds.thy HahnBanach/FunctionNorm.thy		\
    1.50 +  HahnBanach/FunctionOrder.thy HahnBanach/HahnBanach.thy	\
    1.51 +  HahnBanach/HahnBanachExtLemmas.thy				\
    1.52 +  HahnBanach/HahnBanachSupLemmas.thy				\
    1.53 +  HahnBanach/Linearform.thy HahnBanach/NormedSpace.thy	\
    1.54 +  HahnBanach/README.html HahnBanach/ROOT.ML			\
    1.55 +  HahnBanach/Subspace.thy HahnBanach/VectorSpace.thy		\
    1.56 +  HahnBanach/ZornLemma.thy HahnBanach/document/root.bib	\
    1.57 +  HahnBanach/document/root.tex
    1.58 +	@$(ISABELLE_TOOL) usedir -g true $(OUT)/HOL HahnBanach
    1.59  
    1.60  
    1.61  ## HOL-Subst