src/HOL/IsaMakefile
changeset 7393 c6ce498b4767
parent 7392 4137c951b36b
child 7395 66a3d3bb28e4
     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