added the Constructible target
authorpaulson
Wed Jun 19 12:48:55 2002 +0200 (2002-06-19)
changeset 13225b6fc6e4a0a24
parent 13224 6f0928a942d1
child 13226 aea757ff88ce
added the Constructible target
src/ZF/IsaMakefile
     1.1 --- a/src/ZF/IsaMakefile	Wed Jun 19 12:39:41 2002 +0200
     1.2 +++ b/src/ZF/IsaMakefile	Wed Jun 19 12:48:55 2002 +0200
     1.3 @@ -10,7 +10,7 @@
     1.4  images: ZF
     1.5  
     1.6  #Note: keep targets sorted
     1.7 -test: ZF-AC ZF-Coind ZF-IMP ZF-Induct ZF-Resid ZF-UNITY ZF-ex
     1.8 +test: ZF-AC ZF-Coind ZF-Constructible ZF-IMP ZF-Induct ZF-Resid ZF-UNITY ZF-ex
     1.9  all: images test
    1.10  
    1.11  
    1.12 @@ -73,6 +73,18 @@
    1.13  	@$(ISATOOL) usedir $(OUT)/ZF Coind
    1.14  
    1.15  
    1.16 +## ZF-Constructible
    1.17 +
    1.18 +ZF-Constructible: ZF $(LOG)/ZF-Constructible.gz
    1.19 +
    1.20 +$(LOG)/ZF-Constructible.gz: $(OUT)/ZF  Constructible/ROOT.ML \
    1.21 +  Constructible/Formula.thy     Constructible/Relative.thy \
    1.22 +  Constructible/L_axioms.thy    Constructible/Wellorderings.thy \
    1.23 +  Constructible/Normal.thy      Constructible/WF_absolute.thy \
    1.24 +  Constructible/Reflection.thy  Constructible/WFrec.thy
    1.25 +	@$(ISATOOL) usedir $(OUT)/ZF Constructible
    1.26 +
    1.27 +
    1.28  ## ZF-IMP
    1.29  
    1.30  ZF-IMP: ZF $(LOG)/ZF-IMP.gz
    1.31 @@ -134,5 +146,6 @@
    1.32  
    1.33  clean:
    1.34  	@rm -f $(OUT)/ZF $(LOG)/ZF.gz $(LOG)/ZF-AC.gz $(LOG)/ZF-Coind.gz \
    1.35 -	  $(LOG)/ZF-ex.gz $(LOG)/ZF-IMP.gz $(LOG)/ZF-Resid.gz \
    1.36 +	  $(LOG)/ZF-Constructible.gz $(LOG)/ZF-ex.gz \
    1.37 +          $(LOG)/ZF-IMP.gz $(LOG)/ZF-Resid.gz \
    1.38  	  $(LOG)/ZF-UNITY.gz