# HG changeset patch
# User wenzelm
# Date 933182073 -7200
# Node ID df7cf6e8550164ea8d89df6c6b4450a879c00ace
# Parent  78c01842d3b5e1e090391cc529899df391014e27
HOL-Real target now builds an actual image;

diff -r 78c01842d3b5 -r df7cf6e85501 NEWS
--- a/NEWS	Wed Jul 28 18:55:35 1999 +0200
+++ b/NEWS	Wed Jul 28 19:14:33 1999 +0200
@@ -112,6 +112,8 @@
 * Many properties of integer multiplication, division and remainder are now
 available.
 
+* IsaMakefile: the HOL-Real target now builds an actual image;
+
 * New bounded quantifier syntax (input only):
   ! x < y. P, ! x <= y. P, ? x < y. P, ? x <= y. P
 
diff -r 78c01842d3b5 -r df7cf6e85501 src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Wed Jul 28 18:55:35 1999 +0200
+++ b/src/HOL/IsaMakefile	Wed Jul 28 19:14:33 1999 +0200
@@ -7,8 +7,8 @@
 ## targets
 
 default: HOL
-images: HOL TLA
-test: HOL-Subst HOL-Induct HOL-IMP HOL-Hoare HOL-Lex HOL-Real \
+images: HOL HOL-Real TLA
+test: HOL-Subst HOL-Induct HOL-IMP HOL-Hoare HOL-Lex \
   HOL-Auth HOL-UNITY HOL-Modelcheck HOL-Lambda HOL-W0 HOL-MiniML HOL-IOA \
   HOL-AxClasses HOL-AxClasses-Group HOL-AxClasses-Lattice \
   HOL-AxClasses-Tutorial HOL-Quot HOL-ex HOL-Isar_examples TLA-Inc \
@@ -69,6 +69,21 @@
 	@$(ISATOOL) usedir -b $(OUT)/Pure HOL
 
 
+## HOL-Real
+
+HOL-Real: HOL $(OUT)/HOL-Real
+
+$(OUT)/HOL-Real: $(OUT)/HOL \
+  Real/Lubs.ML Real/Lubs.thy Real/PNat.ML Real/PNat.thy \
+  Real/PRat.ML Real/PRat.thy Real/PReal.ML Real/PReal.thy \
+  Real/RComplete.ML Real/RComplete.thy Real/Real.ML Real/Real.thy \
+  Real/RealDef.ML Real/RealDef.thy Real/simproc.ML \
+  Real/RealAbs.ML Real/RealAbs.thy Real/ROOT.ML \
+  Real/Hyperreal/Filter.ML Real/Hyperreal/Filter.thy \
+  Real/Hyperreal/Zorn.ML Real/Hyperreal/Zorn.thy
+	@cd Real; $(ISATOOL) usedir -b $(OUT)/HOL HOL-Real
+
+
 ## HOL-Subst
 
 HOL-Subst: HOL $(LOG)/HOL-Subst.gz
@@ -134,21 +149,6 @@
 	@$(ISATOOL) usedir $(OUT)/HOL Lex
 
 
-## HOL-Real
-
-HOL-Real: HOL $(LOG)/HOL-Real.gz
-
-$(LOG)/HOL-Real.gz: $(OUT)/HOL \
-  Real/Lubs.ML Real/Lubs.thy Real/PNat.ML Real/PNat.thy \
-  Real/PRat.ML Real/PRat.thy Real/PReal.ML Real/PReal.thy \
-  Real/RComplete.ML Real/RComplete.thy Real/Real.ML Real/Real.thy \
-  Real/RealDef.ML Real/RealDef.thy Real/simproc.ML \
-  Real/RealAbs.ML Real/RealAbs.thy Real/ROOT.ML \
-  Real/Hyperreal/Filter.ML Real/Hyperreal/Filter.thy \
-  Real/Hyperreal/Zorn.ML Real/Hyperreal/Zorn.thy
-	@$(ISATOOL) usedir $(OUT)/HOL Real
-
-
 ## HOL-Auth
 
 HOL-Auth: HOL $(LOG)/HOL-Auth.gz
@@ -390,9 +390,9 @@
 ## clean
 
 clean:
-	@rm -f $(OUT)/HOL $(LOG)/HOL.gz $(LOG)/HOL-Subst.gz \
+	@rm -f $(OUT)/HOL $(OUT)/HOL-Real $(LOG)/HOL.gz $(LOG)/HOL-Subst.gz \
 	  $(LOG)/HOL-Induct.gz $(LOG)/HOL-IMP.gz $(LOG)/HOL-Hoare.gz \
-	  $(LOG)/HOL-Lex.gz $(LOG)/HOL-Real.gz $(LOG)/HOL-Auth.gz $(LOG)/HOL-UNITY.gz \
+	  $(LOG)/HOL-Lex.gz $(LOG)/HOL-Auth.gz $(LOG)/HOL-UNITY.gz \
 	  $(LOG)/HOL-Modelcheck.gz $(LOG)/HOL-Lambda.gz $(LOG)/HOL-W0.gz \
 	  $(LOG)/HOL-MiniML.gz $(LOG)/HOL-IOA.gz $(LOG)/HOL-AxClasses.gz \
 	  $(LOG)/HOL-AxClasses-Group.gz $(LOG)/HOL-AxClasses-Lattice.gz \