--- a/src/HOL/IsaMakefile Mon Aug 30 17:26:43 1999 +0200
+++ b/src/HOL/IsaMakefile Mon Aug 30 20:29:28 1999 +0200
@@ -85,6 +85,7 @@
Real/Hyperreal/Zorn.ML Real/Hyperreal/Zorn.thy
@cd Real; $(ISATOOL) usedir -b $(OUT)/HOL HOL-Real
+
## HOL-Real-ex
HOL-Real-ex: HOL-Real $(LOG)/HOL-Real-ex.gz
@@ -92,6 +93,7 @@
$(LOG)/HOL-Real-ex.gz: $(OUT)/HOL-Real Real/ex/ROOT.ML Real/ex/BinEx.ML
@cd Real; $(ISATOOL) usedir $(OUT)/HOL-Real ex
+
## HOL-Subst
HOL-Subst: HOL $(LOG)/HOL-Subst.gz
@@ -401,4 +403,4 @@
$(LOG)/HOL-AxClasses-Tutorial.gz $(LOG)/HOL-Quot.gz \
$(LOG)/HOL-ex.gz $(LOG)/HOL-Isar_examples.gz $(OUT)/TLA \
$(LOG)/TLA.gz $(LOG)/TLA-Inc.gz $(LOG)/TLA-Buffer.gz \
- $(LOG)/TLA-Memory.gz
+ $(LOG)/TLA-Memory.gz $(LOG)/HOL-Real-ex.gz