src/HOL/IsaMakefile
changeset 7392 4137c951b36b
parent 7383 9c4ef0d3f36c
child 7393 c6ce498b4767
     1.1 --- a/src/HOL/IsaMakefile	Mon Aug 30 14:11:47 1999 +0200
     1.2 +++ b/src/HOL/IsaMakefile	Mon Aug 30 15:25:16 1999 +0200
     1.3 @@ -11,8 +11,8 @@
     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 TLA-Inc \
     1.8 -  TLA-Buffer TLA-Memory
     1.9 +  HOL-AxClasses-Tutorial HOL-Quot HOL-ex HOL-Isar_examples HOL-Real-Ex \
    1.10 +  TLA-Inc TLA-Buffer TLA-Memory
    1.11  
    1.12  all: images test
    1.13  
    1.14 @@ -85,6 +85,11 @@
    1.15    Real/Hyperreal/Zorn.ML Real/Hyperreal/Zorn.thy
    1.16  	@cd Real; $(ISATOOL) usedir -b $(OUT)/HOL HOL-Real
    1.17  
    1.18 +## HOL-Real-Ex
    1.19 +
    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  
    1.24  ## HOL-Subst
    1.25