make it actually RUN the real examples
authorpaulson
Mon Aug 30 17:18:20 1999 +0200 (1999-08-30)
changeset 7393c6ce498b4767
parent 7392 4137c951b36b
child 7394 0fc6f18da7c5
make it actually RUN the real examples
src/HOL/IsaMakefile
src/HOL/Real/ex/ROOT.ML
     1.1 --- a/src/HOL/IsaMakefile	Mon Aug 30 15:25:16 1999 +0200
     1.2 +++ b/src/HOL/IsaMakefile	Mon Aug 30 17:18:20 1999 +0200
     1.3 @@ -11,7 +11,7 @@
     1.4  test: HOL-Subst HOL-Induct HOL-IMP HOL-Hoare HOL-Lex \
     1.5    HOL-Auth HOL-UNITY HOL-Modelcheck HOL-Lambda HOL-W0 HOL-MiniML \
     1.6    HOL-IOA HOL-AxClasses-Group HOL-AxClasses-Lattice \
     1.7 -  HOL-AxClasses-Tutorial HOL-Quot HOL-ex HOL-Isar_examples HOL-Real-Ex \
     1.8 +  HOL-AxClasses-Tutorial HOL-Quot HOL-ex HOL-Isar_examples HOL-Real-ex \
     1.9    TLA-Inc TLA-Buffer TLA-Memory
    1.10  
    1.11  all: images test
    1.12 @@ -85,11 +85,12 @@
    1.13    Real/Hyperreal/Zorn.ML Real/Hyperreal/Zorn.thy
    1.14  	@cd Real; $(ISATOOL) usedir -b $(OUT)/HOL HOL-Real
    1.15  
    1.16 -## HOL-Real-Ex
    1.17 +## HOL-Real-ex
    1.18  
    1.19 -HOL-Real-Ex: HOL-Real $(LOG)/HOL-Real-Ex.gz
    1.20 +HOL-Real-ex: HOL-Real $(LOG)/HOL-Real-ex.gz
    1.21  
    1.22 -$(LOG)/HOL-Real-Ex.gz: $(OUT)/HOL-Real Real/ex/ROOT.ML Real/ex/BinEx.ML
    1.23 +$(LOG)/HOL-Real-ex.gz: $(OUT)/HOL-Real Real/ex/ROOT.ML Real/ex/BinEx.ML
    1.24 +	@cd Real; $(ISATOOL) usedir $(OUT)/HOL-Real ex
    1.25  
    1.26  ## HOL-Subst
    1.27  
     2.1 --- a/src/HOL/Real/ex/ROOT.ML	Mon Aug 30 15:25:16 1999 +0200
     2.2 +++ b/src/HOL/Real/ex/ROOT.ML	Mon Aug 30 17:18:20 1999 +0200
     2.3 @@ -10,3 +10,4 @@
     2.4  
     2.5  set proof_timing;
     2.6  
     2.7 +time_use     "BinEx.ML";