author | wenzelm |
Tue, 31 Jan 2006 18:19:32 +0100 | |
changeset 18877 | 2ee8333a2ba1 |
parent 17935 | c6f1442ce949 |
child 22814 | 4cd25f1706bb |
permissions | -rw-r--r-- |
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 |
|
13225 | 13 |
test: ZF-AC ZF-Coind ZF-Constructible ZF-IMP ZF-Induct ZF-Resid ZF-UNITY ZF-ex |
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 |
||
17821 | 26 |
ZF: FOL $(OUT)/ZF$(ML_SUFFIX) |
4518 | 27 |
|
28 |
FOL: |
|
29 |
@cd $(SRC)/FOL; $(ISATOOL) make FOL |
|
2500 | 30 |
|
17821 | 31 |
$(OUT)/ZF$(ML_SUFFIX): $(OUT)/FOL$(ML_SUFFIX) AC.thy Arith.thy \ |
13239 | 32 |
ArithSimp.thy Bool.thy Cardinal.thy \ |
13216 | 33 |
CardinalArith.thy Cardinal_AC.thy \ |
13194 | 34 |
Datatype.ML Datatype.thy Epsilon.thy Finite.thy \ |
13218 | 35 |
Fixedpt.thy Inductive.ML Inductive.thy \ |
13574 | 36 |
InfDatatype.thy Integ/Bin.thy \ |
13560 | 37 |
Integ/EquivClass.thy Integ/Int.thy Integ/IntArith.thy \ |
13520 | 38 |
Integ/IntDiv.thy Integ/int_arith.ML \ |
13780 | 39 |
List.thy Main.ML Main.thy \ |
13171 | 40 |
Main_ZFC.ML Main_ZFC.thy Nat.thy Order.thy OrderArith.thy \ |
13176
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
13171
diff
changeset
|
41 |
OrderType.thy Ordinal.thy OrdQuant.thy Perm.thy \ |
13285 | 42 |
QPair.thy QUniv.thy ROOT.ML \ |
12425 | 43 |
Sum.thy Tools/cartprod.ML Tools/datatype_package.ML \ |
44 |
Tools/ind_cases.ML Tools/induct_tacs.ML Tools/inductive_package.ML \ |
|
45 |
Tools/numeral_syntax.ML Tools/primrec_package.ML Tools/typechk.ML \ |
|
13356 | 46 |
Trancl.thy Univ.thy \ |
13780 | 47 |
WF.thy ZF.thy Zorn.thy arith_data.ML equalities.thy func.thy \ |
17935 | 48 |
ind_syntax.ML pair.thy simpdata.ML upair.thy |
6213 | 49 |
@$(ISATOOL) usedir -b -r $(OUT)/FOL ZF |
2500 | 50 |
|
51 |
||
4518 | 52 |
## ZF-AC |
2500 | 53 |
|
4518 | 54 |
ZF-AC: ZF $(LOG)/ZF-AC.gz |
2500 | 55 |
|
17821 | 56 |
$(LOG)/ZF-AC.gz: $(OUT)/ZF$(ML_SUFFIX) \ |
12776 | 57 |
AC/ROOT.ML AC/AC15_WO6.thy AC/AC16_WO4.thy \ |
58 |
AC/AC16_lemmas.thy AC/AC17_AC1.thy AC/AC18_AC19.thy AC/AC7_AC9.thy \ |
|
59 |
AC/AC_Equiv.thy AC/Cardinal_aux.thy \ |
|
60 |
AC/DC.thy AC/HH.thy AC/Hartog.thy AC/WO1_AC.thy AC/WO1_WO7.thy \ |
|
15083 | 61 |
AC/WO2_AC16.thy AC/WO6_WO1.thy AC/document/root.bib AC/document/root.tex |
62 |
@$(ISATOOL) usedir -g true $(OUT)/ZF AC |
|
2500 | 63 |
|
64 |
||
11479 | 65 |
## ZF-Coind |
4518 | 66 |
|
11479 | 67 |
ZF-Coind: ZF $(LOG)/ZF-Coind.gz |
2500 | 68 |
|
17821 | 69 |
$(LOG)/ZF-Coind.gz: $(OUT)/ZF$(ML_SUFFIX) Coind/Dynamic.thy \ |
12595 | 70 |
Coind/ECR.thy Coind/Language.thy Coind/Map.thy Coind/ROOT.ML \ |
71 |
Coind/Static.thy Coind/Types.thy Coind/Values.thy |
|
11479 | 72 |
@$(ISATOOL) usedir $(OUT)/ZF Coind |
2500 | 73 |
|
74 |
||
13225 | 75 |
## ZF-Constructible |
76 |
||
77 |
ZF-Constructible: ZF $(LOG)/ZF-Constructible.gz |
|
78 |
||
17821 | 79 |
$(LOG)/ZF-Constructible.gz: $(OUT)/ZF$(ML_SUFFIX) Constructible/ROOT.ML \ |
13503 | 80 |
Constructible/Datatype_absolute.thy Constructible/DPow_absolute.thy\ |
13496
6f0c57def6d5
In ZF/Constructible, moved many results from Satisfies_absolute, etc., to
paulson
parents:
13494
diff
changeset
|
81 |
Constructible/Formula.thy Constructible/Internalize.thy \ |
13544 | 82 |
Constructible/AC_in_L.thy Constructible/Relative.thy \ |
13225 | 83 |
Constructible/L_axioms.thy Constructible/Wellorderings.thy \ |
13318 | 84 |
Constructible/MetaExists.thy Constructible/Normal.thy \ |
13634 | 85 |
Constructible/Rank.thy Constructible/Rank_Separation.thy \ |
13339
0f89104dd377
Fixed quantified variable name preservation for ball and bex (bounded quants)
paulson
parents:
13327
diff
changeset
|
86 |
Constructible/Rec_Separation.thy Constructible/Separation.thy \ |
13494 | 87 |
Constructible/Satisfies_absolute.thy Constructible/WF_absolute.thy \ |
13296 | 88 |
Constructible/Reflection.thy Constructible/WFrec.thy \ |
15083 | 89 |
Constructible/document/root.bib Constructible/document/root.tex |
13427 | 90 |
@$(ISATOOL) usedir -g true $(OUT)/ZF Constructible |
13225 | 91 |
|
92 |
||
11479 | 93 |
## ZF-IMP |
94 |
||
95 |
ZF-IMP: ZF $(LOG)/ZF-IMP.gz |
|
96 |
||
17821 | 97 |
$(LOG)/ZF-IMP.gz: $(OUT)/ZF$(ML_SUFFIX) IMP/Com.thy IMP/Denotation.thy IMP/Equiv.thy \ |
12610 | 98 |
IMP/ROOT.ML IMP/document/root.bib IMP/document/root.tex |
11479 | 99 |
@$(ISATOOL) usedir $(OUT)/ZF IMP |
100 |
||
101 |
||
102 |
## ZF-Resid |
|
103 |
||
104 |
ZF-Resid: ZF $(LOG)/ZF-Resid.gz |
|
105 |
||
17821 | 106 |
$(LOG)/ZF-Resid.gz: $(OUT)/ZF$(ML_SUFFIX) Resid/ROOT.ML \ |
12595 | 107 |
Resid/Confluence.thy Resid/Redex.thy \ |
108 |
Resid/Reduction.thy Resid/Residuals.thy Resid/Substitution.thy |
|
11479 | 109 |
@$(ISATOOL) usedir $(OUT)/ZF Resid |
110 |
||
111 |
||
112 |
## ZF-UNITY |
|
113 |
||
114 |
ZF-UNITY: ZF $(LOG)/ZF-UNITY.gz |
|
115 |
||
17821 | 116 |
$(LOG)/ZF-UNITY.gz: $(OUT)/ZF$(ML_SUFFIX) UNITY/ROOT.ML \ |
15634 | 117 |
UNITY/Comp.thy UNITY/Constrains.thy UNITY/FP.thy\ |
118 |
UNITY/GenPrefix.thy UNITY/Guar.thy UNITY/Mutex.thy UNITY/State.thy \ |
|
119 |
UNITY/SubstAx.thy UNITY/UNITY.thy UNITY/Union.thy \ |
|
14076 | 120 |
UNITY/AllocBase.thy UNITY/AllocImpl.thy\ |
14072
f932be305381
Conversion of UNITY/Distributor to Isar script. General tidy-up.
paulson
parents:
14071
diff
changeset
|
121 |
UNITY/ClientImpl.thy UNITY/Distributor.thy\ |
14093
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14092
diff
changeset
|
122 |
UNITY/Follows.thy UNITY/Increasing.thy UNITY/Merge.thy\ |
15634 | 123 |
UNITY/Monotonicity.thy UNITY/MultisetSum.thy UNITY/WFair.thy |
11479 | 124 |
@$(ISATOOL) usedir $(OUT)/ZF UNITY |
125 |
||
126 |
||
12088 | 127 |
## ZF-Induct |
128 |
||
129 |
ZF-Induct: ZF $(LOG)/ZF-Induct.gz |
|
130 |
||
17821 | 131 |
$(LOG)/ZF-Induct.gz: $(OUT)/ZF$(ML_SUFFIX) Induct/ROOT.ML Induct/Acc.thy \ |
12560 | 132 |
Induct/Binary_Trees.thy Induct/Brouwer.thy Induct/Comb.thy \ |
14071 | 133 |
Induct/Datatypes.thy Induct/FoldSet.thy \ |
15201 | 134 |
Induct/ListN.thy Induct/Multiset.thy Induct/Mutil.thy \ |
12560 | 135 |
Induct/Ntree.thy Induct/Primrec.thy Induct/PropLog.thy Induct/Rmap.thy \ |
12207
4dff931b852f
added Induct/Binary_Trees.thy, Induct/Tree_Forest (converted from
wenzelm
parents:
12186
diff
changeset
|
136 |
Induct/Term.thy Induct/Tree_Forest.thy Induct/document/root.tex |
12088 | 137 |
@$(ISATOOL) usedir $(OUT)/ZF Induct |
138 |
||
12175 | 139 |
|
12088 | 140 |
## ZF-ex |
141 |
||
142 |
ZF-ex: ZF $(LOG)/ZF-ex.gz |
|
143 |
||
17821 | 144 |
$(LOG)/ZF-ex.gz: $(OUT)/ZF$(ML_SUFFIX) ex/ROOT.ML \ |
14883 | 145 |
ex/BinEx.thy ex/CoUnit.thy ex/Commutation.thy ex/Group.thy\ |
13085
bfdb0534c8ec
converted theory ex/Limit to Isar script, but it still needs work!
paulson
parents:
12776
diff
changeset
|
146 |
ex/Limit.thy ex/LList.thy ex/Primes.thy \ |
14883 | 147 |
ex/NatSum.thy ex/Ramsey.thy ex/Ring.thy ex/misc.thy |
12088 | 148 |
@$(ISATOOL) usedir $(OUT)/ZF ex |
149 |
||
150 |
||
4518 | 151 |
## clean |
4447 | 152 |
|
153 |
clean: |
|
17821 | 154 |
@rm -f $(OUT)/ZF$(ML_SUFFIX) $(LOG)/ZF.gz $(LOG)/ZF-AC.gz $(LOG)/ZF-Coind.gz \ |
13225 | 155 |
$(LOG)/ZF-Constructible.gz $(LOG)/ZF-ex.gz \ |
156 |
$(LOG)/ZF-IMP.gz $(LOG)/ZF-Resid.gz \ |
|
11479 | 157 |
$(LOG)/ZF-UNITY.gz |