src/HOL/IsaMakefile
changeset 19640 40ec89317425
parent 19564 d3e2f532459a
child 19767 6e77bd331bf4
     1.1 --- a/src/HOL/IsaMakefile	Tue May 16 09:19:12 2006 +0200
     1.2 +++ b/src/HOL/IsaMakefile	Tue May 16 13:01:22 2006 +0200
     1.3 @@ -156,11 +156,11 @@
     1.4  HOL-Complex: HOL $(OUT)/HOL-Complex
     1.5  
     1.6  $(OUT)/HOL-Complex: $(OUT)/HOL Complex/ROOT.ML Library/Zorn.thy			\
     1.7 -  Real/Lubs.thy Real/rat_arith.ML						\
     1.8 -  Real/Rational.thy Real/PReal.thy Real/RComplete.thy				\
     1.9 -  Real/ROOT.ML Real/Real.thy Real/real_arith.ML Real/RealDef.thy		\
    1.10 -  Real/RealPow.thy Real/document/root.tex					\
    1.11 -  Real/Float.thy Real/Float.ML                                                  \
    1.12 +  Real/ContNotDenum.thy Real/Ferrante_Rackoff.thy Real/Float.ML			\
    1.13 +  Real/Float.thy Real/Lubs.thy Real/PReal.thy Real/RComplete.thy		\
    1.14 +  Real/ROOT.ML Real/Rational.thy Real/Real.thy Real/RealDef.thy			\
    1.15 +  Real/RealPow.thy Real/document/root.tex Real/ferrante_rackoff_proof.ML	\
    1.16 +  Real/ferrante_rackoff.ML Real/rat_arith.ML Real/real_arith.ML			\
    1.17    Hyperreal/StarDef.thy Hyperreal/StarClasses.thy				\
    1.18    Hyperreal/EvenOdd.thy Hyperreal/Fact.thy Hyperreal/HLog.thy			\
    1.19    Hyperreal/Filter.thy Hyperreal/HSeries.thy Hyperreal/transfer.ML		\
    1.20 @@ -185,7 +185,7 @@
    1.21  
    1.22  $(LOG)/HOL-Complex-ex.gz: $(OUT)/HOL-Complex Library/Primes.thy \
    1.23    Complex/ex/ROOT.ML Complex/ex/document/root.tex \
    1.24 -  Complex/ex/BigO_Complex.thy Complex/ex/BinEx.thy \
    1.25 +  Complex/ex/BigO_Complex.thy Complex/ex/BinEx.thy Complex/ex/Ferrante_Rackoff_Ex.thy \
    1.26    Complex/ex/NSPrimes.thy Complex/ex/Sqrt.thy Complex/ex/Sqrt_Script.thy
    1.27  	@cd Complex; $(ISATOOL) usedir $(OUT)/HOL-Complex ex
    1.28