src/HOL/IsaMakefile
changeset 7334 a90fc1e5fb19
parent 7307 c065073cdb34
child 7357 d0e16da40ea2
     1.1 --- a/src/HOL/IsaMakefile	Tue Aug 24 11:50:58 1999 +0200
     1.2 +++ b/src/HOL/IsaMakefile	Tue Aug 24 11:54:13 1999 +0200
     1.3 @@ -72,17 +72,14 @@
     1.4  
     1.5  HOL-Real: HOL $(OUT)/HOL-Real
     1.6  
     1.7 -$(OUT)/HOL-Real: $(OUT)/HOL \
     1.8 -  Real/Lubs.ML Real/Lubs.thy Real/PNat.ML Real/PNat.thy \
     1.9 -  Real/PRat.ML Real/PRat.thy Real/PReal.ML Real/PReal.thy \
    1.10 -  Real/RComplete.ML Real/RComplete.thy Real/Real.ML Real/Real.thy \
    1.11 -  Real/RealDef.ML Real/RealDef.thy Real/simproc.ML \
    1.12 -  Real/RealAbs.ML Real/RealAbs.thy Real/ROOT.ML \
    1.13 -  Real/RealBin.ML Real/RealBin.thy \
    1.14 -  Real/RealInt.ML Real/RealInt.thy \
    1.15 -  Real/RealPow.ML Real/RealPow.thy \
    1.16 -  Real/Hyperreal/Filter.ML Real/Hyperreal/Filter.thy \
    1.17 -  Real/Hyperreal/fuf.ML \
    1.18 +$(OUT)/HOL-Real: $(OUT)/HOL Real/Lubs.ML Real/Lubs.thy Real/PNat.ML \
    1.19 +  Real/PNat.thy Real/PRat.ML Real/PRat.thy Real/PReal.ML \
    1.20 +  Real/PReal.thy Real/RComplete.ML Real/RComplete.thy Real/Real.thy \
    1.21 +  Real/RealDef.ML Real/RealDef.thy Real/RealOrd.ML Real/RealOrd.thy \
    1.22 +  Real/simproc.ML Real/RealAbs.ML Real/RealAbs.thy Real/ROOT.ML \
    1.23 +  Real/RealBin.ML Real/RealBin.thy Real/RealInt.ML Real/RealInt.thy \
    1.24 +  Real/RealPow.ML Real/RealPow.thy Real/Hyperreal/Filter.ML \
    1.25 +  Real/Hyperreal/Filter.thy Real/Hyperreal/fuf.ML \
    1.26    Real/Hyperreal/HyperDef.ML Real/Hyperreal/HyperDef.thy \
    1.27    Real/Hyperreal/Zorn.ML Real/Hyperreal/Zorn.thy
    1.28  	@cd Real; $(ISATOOL) usedir -b $(OUT)/HOL HOL-Real