# HG changeset patch
# User paulson
# Date 936026300 -7200
# Node ID c6ce498b47676df288bbd52c938c9629c2b0d826
# Parent  4137c951b36bc852271405b6a58d04b6407872c2
make it actually RUN the real examples

diff -r 4137c951b36b -r c6ce498b4767 src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Mon Aug 30 15:25:16 1999 +0200
+++ b/src/HOL/IsaMakefile	Mon Aug 30 17:18:20 1999 +0200
@@ -11,7 +11,7 @@
 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 HOL-Real-Ex \
+  HOL-AxClasses-Tutorial HOL-Quot HOL-ex HOL-Isar_examples HOL-Real-ex \
   TLA-Inc TLA-Buffer TLA-Memory
 
 all: images test
@@ -85,11 +85,12 @@
   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-Ex: HOL-Real $(LOG)/HOL-Real-Ex.gz
+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
+$(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
 
diff -r 4137c951b36b -r c6ce498b4767 src/HOL/Real/ex/ROOT.ML
--- a/src/HOL/Real/ex/ROOT.ML	Mon Aug 30 15:25:16 1999 +0200
+++ b/src/HOL/Real/ex/ROOT.ML	Mon Aug 30 17:18:20 1999 +0200
@@ -10,3 +10,4 @@
 
 set proof_timing;
 
+time_use     "BinEx.ML";