IsaMakefile for ZF;
authorwenzelm
Thu Jan 09 16:01:34 1997 +0100 (1997-01-09)
changeset 2500777c90aa20b2
parent 2499 0bc87b063447
child 2501 632e126852fc
IsaMakefile for ZF;
src/ZF/IsaMakefile
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/ZF/IsaMakefile	Thu Jan 09 16:01:34 1997 +0100
     1.3 @@ -0,0 +1,97 @@
     1.4 +#
     1.5 +# $Id$
     1.6 +#
     1.7 +# IsaMakefile for ZF
     1.8 +#
     1.9 +
    1.10 +#### Base system
    1.11 +
    1.12 +OUT = $(ISABELLE_OUTPUT_DIR)
    1.13 +
    1.14 +NAMES = ZF upair subset pair domrange \
    1.15 +	func AC equalities Bool \
    1.16 +	Sum QPair mono Fixedpt ind_syntax cartprod add_ind_def \
    1.17 +	constructor intr_elim indrule Inductive Perm Rel EquivClass Trancl \
    1.18 +	WF Order Ordinal Epsilon Arith Univ \
    1.19 +	QUniv Datatype OrderArith OrderType \
    1.20 +	Cardinal CardinalArith Cardinal_AC InfDatatype \
    1.21 +	Zorn Nat Finite List
    1.22 +
    1.23 +FILES = ROOT.ML thy_syntax.ML ../Pure/section_utils.ML simpdata.ML typechk.ML \
    1.24 +	$(NAMES:%=%.thy) $(NAMES:%=%.ML)
    1.25 +
    1.26 +$(OUT)/ZF: $(OUT)/FOL $(FILES)
    1.27 +	@$(ISABELLE) -e "make_html := $(ISABELLE_HTML);" -qu -c $(OUT)/FOL ZF
    1.28 +	@chmod -w $@
    1.29 +
    1.30 +$(OUT)/FOL:
    1.31 +	@cd ../FOL; $(ISATOOL) make
    1.32 +
    1.33 +
    1.34 +
    1.35 +#### Tests and examples
    1.36 +
    1.37 +## IMP-semantics example
    1.38 +
    1.39 +IMP_NAMES = Com Denotation Equiv
    1.40 +IMP_FILES = IMP/ROOT.ML $(IMP_NAMES:%=IMP/%.thy) $(IMP_NAMES:%=IMP/%.ML)
    1.41 +
    1.42 +IMP: $(OUT)/ZF $(IMP_FILES)
    1.43 +	@$(ISATOOL) testdir $(OUT)/ZF IMP
    1.44 +
    1.45 +
    1.46 +## Coinduction example
    1.47 +
    1.48 +COIND_NAMES = ECR MT Map Static Types Values
    1.49 +
    1.50 +COIND_FILES = Coind/ROOT.ML Coind/Language.thy Coind/BCR.thy Coind/Dynamic.thy \
    1.51 +	      $(COIND_NAMES:%=Coind/%.thy) $(COIND_NAMES:%=Coind/%.ML)
    1.52 +
    1.53 +Coind: $(OUT)/ZF $(COIND_FILES)
    1.54 +	@$(ISATOOL) testdir $(OUT)/ZF Coind
    1.55 +
    1.56 +
    1.57 +## AC examples
    1.58 +
    1.59 +AC_NAMES = AC_Equiv Cardinal_aux \
    1.60 +	   AC15_WO6 AC16_WO4 AC16_lemmas AC17_AC1 AC18_AC19 AC1_WO2 \
    1.61 +	   DC DC_lemmas HH Hartog WO1_AC \
    1.62 +	   WO2_AC16 WO6_WO1 WO_AC recfunAC16 rel_is_fun
    1.63 +
    1.64 +AC_FILES = AC/ROOT.ML AC/AC0_AC1.ML AC/AC10_AC15.ML AC/AC1_AC17.ML \
    1.65 +	   AC/AC2_AC6.ML AC/AC7_AC9.ML \
    1.66 +	   AC/WO1_WO6.ML AC/WO1_WO7.ML AC/WO1_WO8.ML \
    1.67 +	   $(AC_NAMES:%=AC/%.thy) $(AC_NAMES:%=AC/%.ML)
    1.68 +
    1.69 +AC: $(OUT)/ZF $(AC_FILES)
    1.70 +	@$(ISATOOL) testdir $(OUT)/ZF AC
    1.71 +
    1.72 +
    1.73 +## Residuals example
    1.74 +
    1.75 +RESID_NAMES = Confluence Redex SubUnion Conversion Reduction Substitution \
    1.76 +	      Cube Residuals Terms
    1.77 +
    1.78 +RESID_FILES = Resid/ROOT.ML $(RESID_NAMES:%=Resid/%.thy) $(RESID_NAMES:%=Resid/%.ML)
    1.79 +
    1.80 +Resid: $(OUT)/ZF $(RESID_FILES)
    1.81 +	@$(ISATOOL) testdir $(OUT)/ZF Resid
    1.82 +
    1.83 +
    1.84 +## Miscellaneous examples
    1.85 +
    1.86 +EX_NAMES = Primes Ramsey Limit Integ twos_compl Bin BT Term TF Ntree Brouwer \
    1.87 +	   Data Enum Rmap Mutil PropLog ListN Acc Comb Primrec LList CoUnit
    1.88 +
    1.89 +EX_FILES = ex/ROOT.ML ex/misc.ML $(EX_NAMES:%=ex/%.thy) $(EX_NAMES:%=ex/%.ML)
    1.90 +
    1.91 +ex: $(OUT)/ZF $(EX_FILES)
    1.92 +	@$(ISATOOL) testdir $(OUT)/ZF ex
    1.93 +
    1.94 +
    1.95 +## Full test
    1.96 +
    1.97 +test: $(OUT)/ZF IMP Coind AC Resid ex
    1.98 +	echo 'Test examples ran successfully' > test
    1.99 +
   1.100 +.PRECIOUS: $(OUT)/FOL $(OUT)/ZF