author  wenzelm 
Tue, 13 Nov 2001 22:20:51 +0100  
changeset 12175  5cf58a1799a7 
parent 12089  34e7693271a9 
child 12186  9b7026a0b0ed 
permissions  rwrr 
2500  1 
# 
2 
# $Id$ 

3 
# 

4 
# IsaMakefile for ZF 

5 
# 

6 

4518  7 
## targets 
2500  8 

4518  9 
default: ZF 
10 
images: ZF 

11479  11 

12 
#Note: keep targets sorted 

12088  13 
test: ZFAC ZFCoind ZFIMP ZFInduct ZFResid ZFUNITY ZFex 
4518  14 
all: images test 
15 

16 

17 
## global settings 

18 

19 
SRC = $(ISABELLE_HOME)/src 

3118  20 
OUT = $(ISABELLE_OUTPUT) 
4447  21 
LOG = $(OUT)/log 
2500  22 

4518  23 

24 
## ZF 

25 

26 
ZF: FOL $(OUT)/ZF 

27 

28 
FOL: 

29 
@cd $(SRC)/FOL; $(ISATOOL) make FOL 

2500  30 

9548  31 
$(OUT)/ZF: $(OUT)/FOL AC.ML AC.thy Arith.ML Arith.thy Bool.ML \ 
32 
arith_data.ML ArithSimp.thy ArithSimp.ML Bool.thy \ 

8812  33 
Cardinal.ML Cardinal.thy CardinalArith.ML CardinalArith.thy \ 
34 
Cardinal_AC.ML Cardinal_AC.thy Datatype.ML Datatype.thy Epsilon.ML \ 

35 
Epsilon.thy Finite.ML Finite.thy Fixedpt.ML Fixedpt.thy Inductive.ML \ 

9578
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
9570
diff
changeset

36 
Inductive.thy InfDatatype.ML InfDatatype.thy \ 
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
9570
diff
changeset

37 
Integ/Bin.ML Integ/Bin.thy \ 
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
9570
diff
changeset

38 
Integ/EquivClass.ML Integ/EquivClass.thy Integ/Int.ML Integ/Int.thy \ 
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
9570
diff
changeset

39 
Integ/IntDiv.ML Integ/IntDiv.thy \ 
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
9570
diff
changeset

40 
Integ/twos_compl.ML Integ/int_arith.ML Integ/IntArith.thy \ 
9570
e16e168984e1
installation of cancellation simprocs for the integers
paulson
parents:
9548
diff
changeset

41 
Let.ML Let.thy List.ML List.thy \ 
8812  42 
Main.thy Nat.ML Nat.thy Order.ML Order.thy OrderArith.ML \ 
43 
OrderArith.thy OrderType.ML OrderType.thy Ordinal.ML Ordinal.thy \ 

44 
Perm.ML Perm.thy QPair.ML QPair.thy QUniv.ML QUniv.thy ROOT.ML \ 

9570
e16e168984e1
installation of cancellation simprocs for the integers
paulson
parents:
9548
diff
changeset

45 
Rel.ML Rel.thy Sum.ML Sum.thy \ 
12175  46 
Tools/numeral_syntax.ML Tools/cartprod.ML \ 
47 
Tools/datatype_package.ML Tools/ind_cases.ML Tools/induct_tacs.ML \ 

8812  48 
Tools/inductive_package.ML Tools/primrec_package.ML Tools/typechk.ML \ 
49 
Trancl.ML Trancl.thy Univ.ML Univ.thy Update.ML Update.thy WF.ML \ 

50 
WF.thy ZF.ML ZF.thy Zorn.ML Zorn.thy domrange.ML domrange.thy \ 

51 
equalities.ML equalities.thy func.ML func.thy ind_syntax.ML mono.ML \ 

52 
mono.thy pair.ML pair.thy simpdata.ML subset.ML subset.thy \ 

53 
thy_syntax.ML upair.ML upair.thy 

6213  54 
@$(ISATOOL) usedir b r $(OUT)/FOL ZF 
2500  55 

56 

4518  57 
## ZFAC 
2500  58 

4518  59 
ZFAC: ZF $(LOG)/ZFAC.gz 
2500  60 

11380  61 
$(LOG)/ZFAC.gz: $(OUT)/ZF \ 
4518  62 
AC/AC15_WO6.ML AC/AC15_WO6.thy AC/AC16_WO4.ML AC/AC16_WO4.thy \ 
63 
AC/AC16_lemmas.ML AC/AC16_lemmas.thy AC/AC17_AC1.ML AC/AC17_AC1.thy \ 

11380  64 
AC/AC18_AC19.ML AC/AC18_AC19.thy AC/AC1_WO2.ML \ 
65 
AC/AC1_WO2.thy AC/AC7_AC9.ML AC/AC_Equiv.ML \ 

4518  66 
AC/AC_Equiv.thy AC/Cardinal_aux.ML AC/Cardinal_aux.thy AC/DC.ML \ 
67 
AC/DC.thy AC/DC_lemmas.ML AC/DC_lemmas.thy AC/HH.ML AC/HH.thy \ 

68 
AC/Hartog.ML AC/Hartog.thy AC/ROOT.ML AC/WO1_AC.ML AC/WO1_AC.thy \ 

11380  69 
AC/WO1_WO7.ML AC/WO1_WO7.thy AC/WO2_AC16.ML \ 
4518  70 
AC/WO2_AC16.thy AC/WO6_WO1.ML AC/WO6_WO1.thy AC/WO_AC.ML AC/WO_AC.thy \ 
71 
AC/recfunAC16.ML AC/recfunAC16.thy AC/rel_is_fun.ML AC/rel_is_fun.thy 

2828  72 
@$(ISATOOL) usedir $(OUT)/ZF AC 
2500  73 

74 

11479  75 
## ZFCoind 
4518  76 

11479  77 
ZFCoind: ZF $(LOG)/ZFCoind.gz 
2500  78 

11479  79 
$(LOG)/ZFCoind.gz: $(OUT)/ZF Coind/BCR.thy Coind/Dynamic.thy \ 
80 
Coind/ECR.ML Coind/ECR.thy Coind/Language.thy Coind/MT.ML Coind/MT.thy \ 

81 
Coind/Map.ML Coind/Map.thy Coind/ROOT.ML Coind/Static.ML \ 

82 
Coind/Static.thy Coind/Types.ML Coind/Types.thy Coind/Values.ML \ 

83 
Coind/Values.thy 

84 
@$(ISATOOL) usedir $(OUT)/ZF Coind 

2500  85 

86 

11479  87 
## ZFIMP 
88 

89 
ZFIMP: ZF $(LOG)/ZFIMP.gz 

90 

91 
$(LOG)/ZFIMP.gz: $(OUT)/ZF IMP/Com.ML IMP/Com.thy IMP/Denotation.ML \ 

92 
IMP/Denotation.thy IMP/Equiv.ML IMP/Equiv.thy IMP/ROOT.ML 

93 
@$(ISATOOL) usedir $(OUT)/ZF IMP 

94 

95 

96 
## ZFResid 

97 

98 
ZFResid: ZF $(LOG)/ZFResid.gz 

99 

100 
$(LOG)/ZFResid.gz: $(OUT)/ZF Resid/Confluence.ML Resid/Confluence.thy \ 

101 
Resid/Conversion.ML Resid/Conversion.thy Resid/Cube.ML Resid/Cube.thy \ 

102 
Resid/ROOT.ML Resid/Redex.ML Resid/Redex.thy Resid/Reduction.ML \ 

103 
Resid/Reduction.thy Resid/Residuals.ML Resid/Residuals.thy \ 

104 
Resid/Substitution.ML \ 

105 
Resid/Substitution.thy Resid/Terms.ML Resid/Terms.thy 

106 
@$(ISATOOL) usedir $(OUT)/ZF Resid 

107 

108 

109 
## ZFUNITY 

110 

111 
ZFUNITY: ZF $(LOG)/ZFUNITY.gz 

112 

113 
$(LOG)/ZFUNITY.gz: $(OUT)/ZF UNITY/ROOT.ML \ 

114 
UNITY/Comp.ML UNITY/Comp.thy UNITY/Constrains.ML UNITY/Constrains.thy \ 

115 
UNITY/FP.ML UNITY/FP.thy UNITY/Guar.ML UNITY/Guar.thy \ 

116 
UNITY/Mutex.ML UNITY/Mutex.thy UNITY/State.ML UNITY/State.thy \ 

117 
UNITY/SubstAx.ML UNITY/SubstAx.thy UNITY/UNITY.ML UNITY/UNITY.thy \ 

118 
UNITY/UNITYMisc.ML UNITY/UNITYMisc.thy UNITY/Union.ML UNITY/Union.thy \ 

119 
UNITY/WFair.ML UNITY/WFair.thy 

120 
@$(ISATOOL) usedir $(OUT)/ZF UNITY 

121 

122 

12088  123 
## ZFInduct 
124 

125 
ZFInduct: ZF $(LOG)/ZFInduct.gz 

126 

127 
$(LOG)/ZFInduct.gz: $(OUT)/ZF Induct/ROOT.ML Induct/Acc.ML Induct/Acc.thy \ 

12089
34e7693271a9
Sidi Ehmety's port of the fold_set operator and multisets to ZF.
paulson
parents:
12088
diff
changeset

128 
Induct/Comb.ML Induct/Comb.thy Induct/FoldSet.ML Induct/FoldSet.thy \ 
12175  129 
Induct/ListN.ML Induct/ListN.thy \ 
130 
Induct/Multiset.ML Induct/Multiset.thy Induct/Mutil.thy \ 

131 
Induct/Primrec_defs.ML Induct/Primrec_defs.thy \ 

132 
Induct/Primrec.ML Induct/Primrec.thy \ 

12088  133 
Induct/PropLog.ML Induct/PropLog.thy Induct/Rmap.ML Induct/Rmap.thy 
134 
@$(ISATOOL) usedir $(OUT)/ZF Induct 

135 

12175  136 

12088  137 
## ZFex 
138 

139 
ZFex: ZF $(LOG)/ZFex.gz 

140 

141 
$(LOG)/ZFex.gz: $(OUT)/ZF ex/ROOT.ML ex/BT.ML ex/BT.thy \ 

142 
ex/BinEx.thy ex/Brouwer.ML ex/Brouwer.thy ex/CoUnit.ML \ 

143 
ex/CoUnit.thy ex/Commutation.ML ex/Commutation.thy \ 

144 
ex/Data.ML ex/Data.thy ex/Enum.ML ex/Enum.thy \ 

145 
ex/Limit.ML ex/Limit.thy ex/LList.ML ex/LList.thy\ 

146 
ex/Ntree.ML ex/Ntree.thy ex/Primes.ML ex/Primes.thy\ 

147 
ex/NatSum.ML ex/NatSum.thy \ 

148 
ex/Ramsey.ML ex/Ramsey.thy ex/TF.ML ex/TF.thy \ 

149 
ex/Term.ML ex/Term.thy ex/misc.thy 

150 
@$(ISATOOL) usedir $(OUT)/ZF ex 

151 

152 

4518  153 
## clean 
4447  154 

155 
clean: 

11479  156 
@rm f $(OUT)/ZF $(LOG)/ZF.gz $(LOG)/ZFAC.gz $(LOG)/ZFCoind.gz \ 
157 
$(LOG)/ZFex.gz $(LOG)/ZFIMP.gz $(LOG)/ZFResid.gz \ 

158 
$(LOG)/ZFUNITY.gz 