--- a/src/HOL/IsaMakefile Mon Aug 30 14:11:47 1999 +0200
+++ b/src/HOL/IsaMakefile Mon Aug 30 15:25:16 1999 +0200
@@ -11,8 +11,8 @@
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-Group HOL-AxClasses-Lattice \
- HOL-AxClasses-Tutorial HOL-Quot HOL-ex HOL-Isar_examples TLA-Inc \
- TLA-Buffer TLA-Memory
+ HOL-AxClasses-Tutorial HOL-Quot HOL-ex HOL-Isar_examples HOL-Real-Ex \
+ TLA-Inc TLA-Buffer TLA-Memory
all: images test
@@ -85,6 +85,11 @@
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
+
+$(LOG)/HOL-Real-Ex.gz: $(OUT)/HOL-Real Real/ex/ROOT.ML Real/ex/BinEx.ML
## HOL-Subst