src/ZF/IsaMakefile
changeset 4518 74c01296e818
parent 4447 b7ee449eb345
child 4878 96578989b0d6
     1.1 --- a/src/ZF/IsaMakefile	Tue Jan 06 12:32:43 1998 +0100
     1.2 +++ b/src/ZF/IsaMakefile	Wed Jan 07 13:53:42 1998 +0100
     1.3 @@ -4,100 +4,118 @@
     1.4  # IsaMakefile for ZF
     1.5  #
     1.6  
     1.7 -#### Base system
     1.8 +## targets
     1.9  
    1.10 +default: ZF
    1.11 +images: ZF
    1.12 +test: ZF-IMP ZF-Coind ZF-AC ZF-Resid ZF-ex
    1.13 +all: images test
    1.14 +
    1.15 +
    1.16 +## global settings
    1.17 +
    1.18 +SRC = $(ISABELLE_HOME)/src
    1.19  OUT = $(ISABELLE_OUTPUT)
    1.20  LOG = $(OUT)/log
    1.21  
    1.22 -NAMES = ZF upair subset pair domrange \
    1.23 -	func AC equalities Bool \
    1.24 -	Sum QPair mono Fixedpt ind_syntax cartprod add_ind_def \
    1.25 -	constructor intr_elim indrule Inductive Perm Rel EquivClass Trancl \
    1.26 -	WF Order Ordinal Epsilon Arith Univ \
    1.27 -	QUniv Datatype OrderArith OrderType \
    1.28 -	Cardinal CardinalArith Cardinal_AC InfDatatype \
    1.29 -	Zorn Nat Finite List
    1.30 +
    1.31 +## ZF
    1.32 +
    1.33 +ZF: FOL $(OUT)/ZF
    1.34 +
    1.35 +FOL:
    1.36 +	@cd $(SRC)/FOL; $(ISATOOL) make FOL
    1.37  
    1.38 -FILES = ROOT.ML thy_syntax.ML ../Pure/section_utils.ML simpdata.ML typechk.ML \
    1.39 -	$(NAMES:%=%.thy) $(NAMES:%=%.ML)
    1.40 -
    1.41 -$(OUT)/ZF: $(OUT)/FOL $(FILES)
    1.42 +$(OUT)/ZF: $(OUT)/FOL $(SRC)/Pure/section_utils.ML AC.ML AC.thy \
    1.43 +  Arith.ML Arith.thy Bool.ML Bool.thy Cardinal.ML Cardinal.thy \
    1.44 +  CardinalArith.ML CardinalArith.thy Cardinal_AC.ML Cardinal_AC.thy \
    1.45 +  Datatype.ML Datatype.thy Epsilon.ML Epsilon.thy EquivClass.ML \
    1.46 +  EquivClass.thy Finite.ML Finite.thy Fixedpt.ML Fixedpt.thy \
    1.47 +  Inductive.ML Inductive.thy InfDatatype.ML InfDatatype.thy List.ML \
    1.48 +  List.thy Nat.ML Nat.thy Order.ML Order.thy OrderArith.ML \
    1.49 +  OrderArith.thy OrderType.ML OrderType.thy Ordinal.ML Ordinal.thy \
    1.50 +  Perm.ML Perm.thy QPair.ML QPair.thy QUniv.ML QUniv.thy ROOT.ML Rel.ML \
    1.51 +  Rel.thy Sum.ML Sum.thy Trancl.ML Trancl.thy Univ.ML Univ.thy WF.ML \
    1.52 +  WF.thy ZF.ML ZF.thy Zorn.ML Zorn.thy add_ind_def.ML add_ind_def.thy \
    1.53 +  cartprod.ML cartprod.thy constructor.ML constructor.thy domrange.ML \
    1.54 +  domrange.thy equalities.ML equalities.thy func.ML func.thy \
    1.55 +  ind_syntax.ML ind_syntax.thy indrule.ML indrule.thy intr_elim.ML \
    1.56 +  intr_elim.thy mono.ML mono.thy pair.ML pair.thy simpdata.ML subset.ML \
    1.57 +  subset.thy thy_syntax.ML typechk.ML upair.ML upair.thy
    1.58  	@$(ISATOOL) usedir -b $(OUT)/FOL ZF
    1.59  
    1.60 -$(OUT)/FOL:
    1.61 -	@cd ../FOL; $(ISATOOL) make
    1.62  
    1.63 -
    1.64 -
    1.65 -#### Tests and examples
    1.66 +## ZF-IMP
    1.67  
    1.68 -## IMP-semantics example
    1.69 +ZF-IMP: ZF $(LOG)/ZF-IMP.gz
    1.70  
    1.71 -IMP_NAMES = Com Denotation Equiv
    1.72 -IMP_FILES = IMP/ROOT.ML $(IMP_NAMES:%=IMP/%.thy) $(IMP_NAMES:%=IMP/%.ML)
    1.73 -
    1.74 -$(LOG)/ZF-IMP.gz: $(OUT)/ZF $(IMP_FILES)
    1.75 +$(LOG)/ZF-IMP.gz: $(OUT)/ZF IMP/Com.ML IMP/Com.thy IMP/Denotation.ML \
    1.76 +  IMP/Denotation.thy IMP/Equiv.ML IMP/Equiv.thy IMP/ROOT.ML
    1.77  	@$(ISATOOL) usedir $(OUT)/ZF IMP
    1.78  
    1.79  
    1.80 -## Coinduction example
    1.81 +## ZF-Coind
    1.82  
    1.83 -COIND_NAMES = ECR MT Map Static Types Values
    1.84 +ZF-Coind: ZF $(LOG)/ZF-Coind.gz
    1.85  
    1.86 -COIND_FILES = Coind/ROOT.ML Coind/Language.thy Coind/BCR.thy Coind/Dynamic.thy \
    1.87 -	      $(COIND_NAMES:%=Coind/%.thy) $(COIND_NAMES:%=Coind/%.ML)
    1.88 -
    1.89 -$(LOG)/ZF-Coind.gz: $(OUT)/ZF $(COIND_FILES)
    1.90 +$(LOG)/ZF-Coind.gz: $(OUT)/ZF Coind/BCR.thy Coind/Dynamic.thy \
    1.91 +  Coind/ECR.ML Coind/ECR.thy Coind/Language.thy Coind/MT.ML Coind/MT.thy \
    1.92 +  Coind/Map.ML Coind/Map.thy Coind/ROOT.ML Coind/Static.ML \
    1.93 +  Coind/Static.thy Coind/Types.ML Coind/Types.thy Coind/Values.ML \
    1.94 +  Coind/Values.thy
    1.95  	@$(ISATOOL) usedir $(OUT)/ZF Coind
    1.96  
    1.97  
    1.98 -## AC examples
    1.99 +## ZF-AC
   1.100  
   1.101 -AC_NAMES = AC_Equiv Cardinal_aux \
   1.102 -	   AC15_WO6 AC16_WO4 AC16_lemmas AC17_AC1 AC18_AC19 AC1_WO2 \
   1.103 -	   DC DC_lemmas HH Hartog WO1_AC \
   1.104 -	   WO2_AC16 WO6_WO1 WO_AC recfunAC16 rel_is_fun
   1.105 +ZF-AC: ZF $(LOG)/ZF-AC.gz
   1.106  
   1.107 -AC_FILES = AC/ROOT.ML AC/AC0_AC1.ML AC/AC10_AC15.ML AC/AC1_AC17.ML \
   1.108 -	   AC/AC2_AC6.ML AC/AC7_AC9.ML \
   1.109 -	   AC/WO1_WO6.ML AC/WO1_WO7.ML AC/WO1_WO8.ML \
   1.110 -	   $(AC_NAMES:%=AC/%.thy) $(AC_NAMES:%=AC/%.ML)
   1.111 -
   1.112 -$(LOG)/ZF-AC.gz: $(OUT)/ZF $(AC_FILES)
   1.113 +$(LOG)/ZF-AC.gz: $(OUT)/ZF AC/AC0_AC1.ML AC/AC10_AC15.ML \
   1.114 +  AC/AC15_WO6.ML AC/AC15_WO6.thy AC/AC16_WO4.ML AC/AC16_WO4.thy \
   1.115 +  AC/AC16_lemmas.ML AC/AC16_lemmas.thy AC/AC17_AC1.ML AC/AC17_AC1.thy \
   1.116 +  AC/AC18_AC19.ML AC/AC18_AC19.thy AC/AC1_AC17.ML AC/AC1_WO2.ML \
   1.117 +  AC/AC1_WO2.thy AC/AC2_AC6.ML AC/AC7_AC9.ML AC/AC_Equiv.ML \
   1.118 +  AC/AC_Equiv.thy AC/Cardinal_aux.ML AC/Cardinal_aux.thy AC/DC.ML \
   1.119 +  AC/DC.thy AC/DC_lemmas.ML AC/DC_lemmas.thy AC/HH.ML AC/HH.thy \
   1.120 +  AC/Hartog.ML AC/Hartog.thy AC/ROOT.ML AC/WO1_AC.ML AC/WO1_AC.thy \
   1.121 +  AC/WO1_WO6.ML AC/WO1_WO7.ML AC/WO1_WO8.ML AC/WO2_AC16.ML \
   1.122 +  AC/WO2_AC16.thy AC/WO6_WO1.ML AC/WO6_WO1.thy AC/WO_AC.ML AC/WO_AC.thy \
   1.123 +  AC/recfunAC16.ML AC/recfunAC16.thy AC/rel_is_fun.ML AC/rel_is_fun.thy
   1.124  	@$(ISATOOL) usedir $(OUT)/ZF AC
   1.125  
   1.126  
   1.127 -## Residuals example
   1.128 +## ZF-Resid
   1.129 +
   1.130 +ZF-Resid: ZF $(LOG)/ZF-Resid.gz
   1.131  
   1.132 -RESID_NAMES = Confluence Redex SubUnion Conversion Reduction Substitution \
   1.133 -	      Cube Residuals Terms
   1.134 -
   1.135 -RESID_FILES = Resid/ROOT.ML $(RESID_NAMES:%=Resid/%.thy) $(RESID_NAMES:%=Resid/%.ML)
   1.136 -
   1.137 -$(LOG)/ZF-Resid.gz: $(OUT)/ZF $(RESID_FILES)
   1.138 +$(LOG)/ZF-Resid.gz: $(OUT)/ZF Resid/Confluence.ML Resid/Confluence.thy \
   1.139 +  Resid/Conversion.ML Resid/Conversion.thy Resid/Cube.ML Resid/Cube.thy \
   1.140 +  Resid/ROOT.ML Resid/Redex.ML Resid/Redex.thy Resid/Reduction.ML \
   1.141 +  Resid/Reduction.thy Resid/Residuals.ML Resid/Residuals.thy \
   1.142 +  Resid/SubUnion.ML Resid/SubUnion.thy Resid/Substitution.ML \
   1.143 +  Resid/Substitution.thy Resid/Terms.ML Resid/Terms.thy
   1.144  	@$(ISATOOL) usedir $(OUT)/ZF Resid
   1.145  
   1.146  
   1.147 -## Miscellaneous examples
   1.148 +## ZF-ex
   1.149 +
   1.150 +ZF-ex: ZF $(LOG)/ZF-ex.gz
   1.151  
   1.152 -EX_NAMES = Primes Ramsey Limit Integ twos_compl Bin BT Term TF Ntree Brouwer \
   1.153 -	   Data Enum Rmap Mutil PropLog ListN Acc Comb Primrec LList CoUnit
   1.154 -
   1.155 -EX_FILES = ex/ROOT.ML ex/misc.ML $(EX_NAMES:%=ex/%.thy) $(EX_NAMES:%=ex/%.ML)
   1.156 -
   1.157 -$(LOG)/ZF-ex.gz: $(OUT)/ZF $(EX_FILES)
   1.158 +$(LOG)/ZF-ex.gz: $(OUT)/ZF ex/Acc.ML ex/Acc.thy ex/BT.ML ex/BT.thy \
   1.159 +  ex/Bin.ML ex/Bin.thy ex/Brouwer.ML ex/Brouwer.thy ex/CoUnit.ML \
   1.160 +  ex/CoUnit.thy ex/Comb.ML ex/Comb.thy ex/Data.ML ex/Data.thy ex/Enum.ML \
   1.161 +  ex/Enum.thy ex/Integ.ML ex/Integ.thy ex/LList.ML ex/LList.thy \
   1.162 +  ex/Limit.ML ex/Limit.thy ex/ListN.ML ex/ListN.thy ex/Mutil.ML \
   1.163 +  ex/Mutil.thy ex/Ntree.ML ex/Ntree.thy ex/Primes.ML ex/Primes.thy \
   1.164 +  ex/Primrec.ML ex/Primrec.thy ex/PropLog.ML ex/PropLog.thy ex/ROOT.ML \
   1.165 +  ex/Ramsey.ML ex/Ramsey.thy ex/Rmap.ML ex/Rmap.thy ex/TF.ML ex/TF.thy \
   1.166 +  ex/Term.ML ex/Term.thy ex/misc.ML ex/twos_compl.ML ex/twos_compl.thy
   1.167  	@$(ISATOOL) usedir $(OUT)/ZF ex
   1.168  
   1.169  
   1.170 -## Full test
   1.171 -
   1.172 -ALL_TARGETS = $(OUT)/ZF $(LOG)/ZF-IMP.gz $(LOG)/ZF-Coind.gz \
   1.173 -  $(LOG)/ZF-AC.gz $(LOG)/ZF-Resid.gz $(LOG)/ZF-ex.gz
   1.174 -
   1.175 -test: $(ALL_TARGETS)
   1.176 +## clean
   1.177  
   1.178  clean:
   1.179 -	@rm -f $(ALL_TARGETS)
   1.180 -
   1.181 -
   1.182 -.PRECIOUS: $(OUT)/FOL $(OUT)/ZF
   1.183 +	@rm -f $(OUT)/ZF $(LOG)/ZF.gz $(LOG)/ZF-IMP.gz \
   1.184 +	  $(LOG)/ZF-Coind.gz $(LOG)/ZF-AC.gz $(LOG)/ZF-Resid.gz \
   1.185 +	  $(LOG)/ZF-ex.gz