1.1 --- a/NEWS	Wed Jul 28 18:55:35 1999 +0200
     1.2 +++ b/NEWS	Wed Jul 28 19:14:33 1999 +0200
     1.3 @@ -112,6 +112,8 @@
     1.4  * Many properties of integer multiplication, division and remainder are now
     1.5  available.
     1.6  
     1.7 +* IsaMakefile: the HOL-Real target now builds an actual image;
     1.8 +
     1.9  * New bounded quantifier syntax (input only):
    1.10    ! x < y. P, ! x <= y. P, ? x < y. P, ? x <= y. P
    1.11  

     2.1 --- a/src/HOL/IsaMakefile	Wed Jul 28 18:55:35 1999 +0200
     2.2 +++ b/src/HOL/IsaMakefile	Wed Jul 28 19:14:33 1999 +0200
     2.3 @@ -7,8 +7,8 @@
     2.4  ## targets
     2.5  
     2.6  default: HOL
     2.7 -images: HOL TLA
     2.8 -test: HOL-Subst HOL-Induct HOL-IMP HOL-Hoare HOL-Lex HOL-Real \
     2.9 +images: HOL HOL-Real TLA
    2.10 +test: HOL-Subst HOL-Induct HOL-IMP HOL-Hoare HOL-Lex \
    2.11    HOL-Auth HOL-UNITY HOL-Modelcheck HOL-Lambda HOL-W0 HOL-MiniML HOL-IOA \
    2.12    HOL-AxClasses HOL-AxClasses-Group HOL-AxClasses-Lattice \
    2.13    HOL-AxClasses-Tutorial HOL-Quot HOL-ex HOL-Isar_examples TLA-Inc \
    2.14 @@ -69,6 +69,21 @@
    2.15  	@$(ISATOOL) usedir -b $(OUT)/Pure HOL
    2.16  
    2.17  
    2.18 +## HOL-Real
    2.19 +
    2.20 +HOL-Real: HOL $(OUT)/HOL-Real
    2.21 +
    2.22 +$(OUT)/HOL-Real: $(OUT)/HOL \
    2.23 +  Real/Lubs.ML Real/Lubs.thy Real/PNat.ML Real/PNat.thy \
    2.24 +  Real/PRat.ML Real/PRat.thy Real/PReal.ML Real/PReal.thy \
    2.25 +  Real/RComplete.ML Real/RComplete.thy Real/Real.ML Real/Real.thy \
    2.26 +  Real/RealDef.ML Real/RealDef.thy Real/simproc.ML \
    2.27 +  Real/RealAbs.ML Real/RealAbs.thy Real/ROOT.ML \
    2.28 +  Real/Hyperreal/Filter.ML Real/Hyperreal/Filter.thy \
    2.29 +  Real/Hyperreal/Zorn.ML Real/Hyperreal/Zorn.thy
    2.30 +	@cd Real; $(ISATOOL) usedir -b $(OUT)/HOL HOL-Real
    2.31 +
    2.32 +
    2.33  ## HOL-Subst
    2.34  
    2.35  HOL-Subst: HOL $(LOG)/HOL-Subst.gz
    2.36 @@ -134,21 +149,6 @@
    2.37  	@$(ISATOOL) usedir $(OUT)/HOL Lex
    2.38  
    2.39  
    2.40 -## HOL-Real
    2.41 -
    2.42 -HOL-Real: HOL $(LOG)/HOL-Real.gz
    2.43 -
    2.44 -$(LOG)/HOL-Real.gz: $(OUT)/HOL \
    2.45 -  Real/Lubs.ML Real/Lubs.thy Real/PNat.ML Real/PNat.thy \
    2.46 -  Real/PRat.ML Real/PRat.thy Real/PReal.ML Real/PReal.thy \
    2.47 -  Real/RComplete.ML Real/RComplete.thy Real/Real.ML Real/Real.thy \
    2.48 -  Real/RealDef.ML Real/RealDef.thy Real/simproc.ML \
    2.49 -  Real/RealAbs.ML Real/RealAbs.thy Real/ROOT.ML \
    2.50 -  Real/Hyperreal/Filter.ML Real/Hyperreal/Filter.thy \
    2.51 -  Real/Hyperreal/Zorn.ML Real/Hyperreal/Zorn.thy
    2.52 -	@$(ISATOOL) usedir $(OUT)/HOL Real
    2.53 -
    2.54 -
    2.55  ## HOL-Auth
    2.56  
    2.57  HOL-Auth: HOL $(LOG)/HOL-Auth.gz
    2.58 @@ -390,9 +390,9 @@
    2.59  ## clean
    2.60  
    2.61  clean:
    2.62 -	@rm -f $(OUT)/HOL $(LOG)/HOL.gz $(LOG)/HOL-Subst.gz \
    2.63 +	@rm -f $(OUT)/HOL $(OUT)/HOL-Real $(LOG)/HOL.gz $(LOG)/HOL-Subst.gz \
    2.64  	  $(LOG)/HOL-Induct.gz $(LOG)/HOL-IMP.gz $(LOG)/HOL-Hoare.gz \
    2.65 -	  $(LOG)/HOL-Lex.gz $(LOG)/HOL-Real.gz $(LOG)/HOL-Auth.gz $(LOG)/HOL-UNITY.gz \
    2.66 +	  $(LOG)/HOL-Lex.gz $(LOG)/HOL-Auth.gz $(LOG)/HOL-UNITY.gz \
    2.67  	  $(LOG)/HOL-Modelcheck.gz $(LOG)/HOL-Lambda.gz $(LOG)/HOL-W0.gz \
    2.68  	  $(LOG)/HOL-MiniML.gz $(LOG)/HOL-IOA.gz $(LOG)/HOL-AxClasses.gz \
    2.69  	  $(LOG)/HOL-AxClasses-Group.gz $(LOG)/HOL-AxClasses-Lattice.gz \