src/HOL/IsaMakefile

 default: HOL
 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-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
 
 
 ## global settings

   Real/Hyperreal/Filter.thy Real/Hyperreal/fuf.ML \
   Real/Hyperreal/HyperDef.ML Real/Hyperreal/HyperDef.thy \
   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
 
 HOL-Subst: HOL $(LOG)/HOL-Subst.gz