src/HOL/IsaMakefile
changeset 7125 df7cf6e85501
parent 7085 e5a5f8d23f26
child 7142 89e0ff71d113
     1.1 --- a/src/HOL/IsaMakefile	Wed Jul 28 18:55:35 1999 +0200
     1.2 +++ b/src/HOL/IsaMakefile	Wed Jul 28 19:14:33 1999 +0200
     1.3 @@ -7,8 +7,8 @@
     1.4  ## targets
     1.5  
     1.6  default: HOL
     1.7 -images: HOL TLA
     1.8 -test: HOL-Subst HOL-Induct HOL-IMP HOL-Hoare HOL-Lex HOL-Real \
     1.9 +images: HOL HOL-Real TLA
    1.10 +test: HOL-Subst HOL-Induct HOL-IMP HOL-Hoare HOL-Lex \
    1.11    HOL-Auth HOL-UNITY HOL-Modelcheck HOL-Lambda HOL-W0 HOL-MiniML HOL-IOA \
    1.12    HOL-AxClasses HOL-AxClasses-Group HOL-AxClasses-Lattice \
    1.13    HOL-AxClasses-Tutorial HOL-Quot HOL-ex HOL-Isar_examples TLA-Inc \
    1.14 @@ -69,6 +69,21 @@
    1.15  	@$(ISATOOL) usedir -b $(OUT)/Pure HOL
    1.16  
    1.17  
    1.18 +## HOL-Real
    1.19 +
    1.20 +HOL-Real: HOL $(OUT)/HOL-Real
    1.21 +
    1.22 +$(OUT)/HOL-Real: $(OUT)/HOL \
    1.23 +  Real/Lubs.ML Real/Lubs.thy Real/PNat.ML Real/PNat.thy \
    1.24 +  Real/PRat.ML Real/PRat.thy Real/PReal.ML Real/PReal.thy \
    1.25 +  Real/RComplete.ML Real/RComplete.thy Real/Real.ML Real/Real.thy \
    1.26 +  Real/RealDef.ML Real/RealDef.thy Real/simproc.ML \
    1.27 +  Real/RealAbs.ML Real/RealAbs.thy Real/ROOT.ML \
    1.28 +  Real/Hyperreal/Filter.ML Real/Hyperreal/Filter.thy \
    1.29 +  Real/Hyperreal/Zorn.ML Real/Hyperreal/Zorn.thy
    1.30 +	@cd Real; $(ISATOOL) usedir -b $(OUT)/HOL HOL-Real
    1.31 +
    1.32 +
    1.33  ## HOL-Subst
    1.34  
    1.35  HOL-Subst: HOL $(LOG)/HOL-Subst.gz
    1.36 @@ -134,21 +149,6 @@
    1.37  	@$(ISATOOL) usedir $(OUT)/HOL Lex
    1.38  
    1.39  
    1.40 -## HOL-Real
    1.41 -
    1.42 -HOL-Real: HOL $(LOG)/HOL-Real.gz
    1.43 -
    1.44 -$(LOG)/HOL-Real.gz: $(OUT)/HOL \
    1.45 -  Real/Lubs.ML Real/Lubs.thy Real/PNat.ML Real/PNat.thy \
    1.46 -  Real/PRat.ML Real/PRat.thy Real/PReal.ML Real/PReal.thy \
    1.47 -  Real/RComplete.ML Real/RComplete.thy Real/Real.ML Real/Real.thy \
    1.48 -  Real/RealDef.ML Real/RealDef.thy Real/simproc.ML \
    1.49 -  Real/RealAbs.ML Real/RealAbs.thy Real/ROOT.ML \
    1.50 -  Real/Hyperreal/Filter.ML Real/Hyperreal/Filter.thy \
    1.51 -  Real/Hyperreal/Zorn.ML Real/Hyperreal/Zorn.thy
    1.52 -	@$(ISATOOL) usedir $(OUT)/HOL Real
    1.53 -
    1.54 -
    1.55  ## HOL-Auth
    1.56  
    1.57  HOL-Auth: HOL $(LOG)/HOL-Auth.gz
    1.58 @@ -390,9 +390,9 @@
    1.59  ## clean
    1.60  
    1.61  clean:
    1.62 -	@rm -f $(OUT)/HOL $(LOG)/HOL.gz $(LOG)/HOL-Subst.gz \
    1.63 +	@rm -f $(OUT)/HOL $(OUT)/HOL-Real $(LOG)/HOL.gz $(LOG)/HOL-Subst.gz \
    1.64  	  $(LOG)/HOL-Induct.gz $(LOG)/HOL-IMP.gz $(LOG)/HOL-Hoare.gz \
    1.65 -	  $(LOG)/HOL-Lex.gz $(LOG)/HOL-Real.gz $(LOG)/HOL-Auth.gz $(LOG)/HOL-UNITY.gz \
    1.66 +	  $(LOG)/HOL-Lex.gz $(LOG)/HOL-Auth.gz $(LOG)/HOL-UNITY.gz \
    1.67  	  $(LOG)/HOL-Modelcheck.gz $(LOG)/HOL-Lambda.gz $(LOG)/HOL-W0.gz \
    1.68  	  $(LOG)/HOL-MiniML.gz $(LOG)/HOL-IOA.gz $(LOG)/HOL-AxClasses.gz \
    1.69  	  $(LOG)/HOL-AxClasses-Group.gz $(LOG)/HOL-AxClasses-Lattice.gz \