src/ZF/IsaMakefile
author wenzelm
Fri Dec 19 10:18:58 1997 +0100 (1997-12-19)
changeset 4447 b7ee449eb345
parent 3505 1cb4ea47d967
child 4518 74c01296e818
permissions -rw-r--r--
log files;
'clean' target;
wenzelm@2500
     1
#
wenzelm@2500
     2
# $Id$
wenzelm@2500
     3
#
wenzelm@2500
     4
# IsaMakefile for ZF
wenzelm@2500
     5
#
wenzelm@2500
     6
wenzelm@2500
     7
#### Base system
wenzelm@2500
     8
wenzelm@3118
     9
OUT = $(ISABELLE_OUTPUT)
wenzelm@4447
    10
LOG = $(OUT)/log
wenzelm@2500
    11
wenzelm@2500
    12
NAMES = ZF upair subset pair domrange \
wenzelm@2500
    13
	func AC equalities Bool \
wenzelm@2500
    14
	Sum QPair mono Fixedpt ind_syntax cartprod add_ind_def \
wenzelm@2500
    15
	constructor intr_elim indrule Inductive Perm Rel EquivClass Trancl \
wenzelm@2500
    16
	WF Order Ordinal Epsilon Arith Univ \
wenzelm@2500
    17
	QUniv Datatype OrderArith OrderType \
wenzelm@2500
    18
	Cardinal CardinalArith Cardinal_AC InfDatatype \
wenzelm@2500
    19
	Zorn Nat Finite List
wenzelm@2500
    20
wenzelm@2500
    21
FILES = ROOT.ML thy_syntax.ML ../Pure/section_utils.ML simpdata.ML typechk.ML \
wenzelm@2500
    22
	$(NAMES:%=%.thy) $(NAMES:%=%.ML)
wenzelm@2500
    23
wenzelm@2500
    24
$(OUT)/ZF: $(OUT)/FOL $(FILES)
wenzelm@3057
    25
	@$(ISATOOL) usedir -b $(OUT)/FOL ZF
wenzelm@2500
    26
wenzelm@2500
    27
$(OUT)/FOL:
wenzelm@2500
    28
	@cd ../FOL; $(ISATOOL) make
wenzelm@2500
    29
wenzelm@2500
    30
wenzelm@2500
    31
wenzelm@2500
    32
#### Tests and examples
wenzelm@2500
    33
wenzelm@2500
    34
## IMP-semantics example
wenzelm@2500
    35
wenzelm@2500
    36
IMP_NAMES = Com Denotation Equiv
wenzelm@2500
    37
IMP_FILES = IMP/ROOT.ML $(IMP_NAMES:%=IMP/%.thy) $(IMP_NAMES:%=IMP/%.ML)
wenzelm@2500
    38
wenzelm@4447
    39
$(LOG)/ZF-IMP.gz: $(OUT)/ZF $(IMP_FILES)
wenzelm@2828
    40
	@$(ISATOOL) usedir $(OUT)/ZF IMP
wenzelm@2500
    41
wenzelm@2500
    42
wenzelm@2500
    43
## Coinduction example
wenzelm@2500
    44
wenzelm@2500
    45
COIND_NAMES = ECR MT Map Static Types Values
wenzelm@2500
    46
wenzelm@2500
    47
COIND_FILES = Coind/ROOT.ML Coind/Language.thy Coind/BCR.thy Coind/Dynamic.thy \
wenzelm@2500
    48
	      $(COIND_NAMES:%=Coind/%.thy) $(COIND_NAMES:%=Coind/%.ML)
wenzelm@2500
    49
wenzelm@4447
    50
$(LOG)/ZF-Coind.gz: $(OUT)/ZF $(COIND_FILES)
wenzelm@2828
    51
	@$(ISATOOL) usedir $(OUT)/ZF Coind
wenzelm@2500
    52
wenzelm@2500
    53
wenzelm@2500
    54
## AC examples
wenzelm@2500
    55
wenzelm@2500
    56
AC_NAMES = AC_Equiv Cardinal_aux \
wenzelm@2500
    57
	   AC15_WO6 AC16_WO4 AC16_lemmas AC17_AC1 AC18_AC19 AC1_WO2 \
wenzelm@2500
    58
	   DC DC_lemmas HH Hartog WO1_AC \
wenzelm@2500
    59
	   WO2_AC16 WO6_WO1 WO_AC recfunAC16 rel_is_fun
wenzelm@2500
    60
wenzelm@2500
    61
AC_FILES = AC/ROOT.ML AC/AC0_AC1.ML AC/AC10_AC15.ML AC/AC1_AC17.ML \
wenzelm@2500
    62
	   AC/AC2_AC6.ML AC/AC7_AC9.ML \
wenzelm@2500
    63
	   AC/WO1_WO6.ML AC/WO1_WO7.ML AC/WO1_WO8.ML \
wenzelm@2500
    64
	   $(AC_NAMES:%=AC/%.thy) $(AC_NAMES:%=AC/%.ML)
wenzelm@2500
    65
wenzelm@4447
    66
$(LOG)/ZF-AC.gz: $(OUT)/ZF $(AC_FILES)
wenzelm@2828
    67
	@$(ISATOOL) usedir $(OUT)/ZF AC
wenzelm@2500
    68
wenzelm@2500
    69
wenzelm@2500
    70
## Residuals example
wenzelm@2500
    71
wenzelm@2500
    72
RESID_NAMES = Confluence Redex SubUnion Conversion Reduction Substitution \
wenzelm@2500
    73
	      Cube Residuals Terms
wenzelm@2500
    74
wenzelm@2500
    75
RESID_FILES = Resid/ROOT.ML $(RESID_NAMES:%=Resid/%.thy) $(RESID_NAMES:%=Resid/%.ML)
wenzelm@2500
    76
wenzelm@4447
    77
$(LOG)/ZF-Resid.gz: $(OUT)/ZF $(RESID_FILES)
wenzelm@2828
    78
	@$(ISATOOL) usedir $(OUT)/ZF Resid
wenzelm@2500
    79
wenzelm@2500
    80
wenzelm@2500
    81
## Miscellaneous examples
wenzelm@2500
    82
wenzelm@2500
    83
EX_NAMES = Primes Ramsey Limit Integ twos_compl Bin BT Term TF Ntree Brouwer \
wenzelm@2500
    84
	   Data Enum Rmap Mutil PropLog ListN Acc Comb Primrec LList CoUnit
wenzelm@2500
    85
wenzelm@2500
    86
EX_FILES = ex/ROOT.ML ex/misc.ML $(EX_NAMES:%=ex/%.thy) $(EX_NAMES:%=ex/%.ML)
wenzelm@2500
    87
wenzelm@4447
    88
$(LOG)/ZF-ex.gz: $(OUT)/ZF $(EX_FILES)
wenzelm@2828
    89
	@$(ISATOOL) usedir $(OUT)/ZF ex
wenzelm@2500
    90
wenzelm@2500
    91
wenzelm@2500
    92
## Full test
wenzelm@2500
    93
wenzelm@4447
    94
ALL_TARGETS = $(OUT)/ZF $(LOG)/ZF-IMP.gz $(LOG)/ZF-Coind.gz \
wenzelm@4447
    95
  $(LOG)/ZF-AC.gz $(LOG)/ZF-Resid.gz $(LOG)/ZF-ex.gz
wenzelm@4447
    96
wenzelm@4447
    97
test: $(ALL_TARGETS)
wenzelm@4447
    98
wenzelm@4447
    99
clean:
wenzelm@4447
   100
	@rm -f $(ALL_TARGETS)
wenzelm@4447
   101
wenzelm@2500
   102
wenzelm@2500
   103
.PRECIOUS: $(OUT)/FOL $(OUT)/ZF