author | wenzelm |
Sun, 22 Aug 2010 19:33:01 +0200 | |
changeset 38578 | 1ebc6b76e5ff |
parent 37781 | 2fbbf0a48cef |
child 42138 | e54a985daa61 |
permissions | -rw-r--r-- |
2500 | 1 |
# |
2 |
# IsaMakefile for ZF |
|
3 |
# |
|
4 |
||
4518 | 5 |
## targets |
2500 | 6 |
|
4518 | 7 |
default: ZF |
8 |
images: ZF |
|
11479 | 9 |
|
10 |
#Note: keep targets sorted |
|
13225 | 11 |
test: ZF-AC ZF-Coind ZF-Constructible ZF-IMP ZF-Induct ZF-Resid ZF-UNITY ZF-ex |
4518 | 12 |
all: images test |
13 |
||
14 |
||
15 |
## global settings |
|
16 |
||
17 |
SRC = $(ISABELLE_HOME)/src |
|
3118 | 18 |
OUT = $(ISABELLE_OUTPUT) |
4447 | 19 |
LOG = $(OUT)/log |
2500 | 20 |
|
4518 | 21 |
|
22 |
## ZF |
|
23 |
||
27203 | 24 |
ZF: FOL $(OUT)/ZF |
4518 | 25 |
|
26 |
FOL: |
|
28500 | 27 |
@cd $(SRC)/FOL; $(ISABELLE_TOOL) make FOL |
2500 | 28 |
|
37781
2fbbf0a48cef
moved misc legacy stuff from OldGoals to Misc_Legacy;
wenzelm
parents:
36862
diff
changeset
|
29 |
$(OUT)/ZF: $(OUT)/FOL $(SRC)/Tools/misc_legacy.ML AC.thy Arith.thy \ |
2fbbf0a48cef
moved misc legacy stuff from OldGoals to Misc_Legacy;
wenzelm
parents:
36862
diff
changeset
|
30 |
ArithSimp.thy Bin.thy Bool.thy Cardinal.thy CardinalArith.thy \ |
2fbbf0a48cef
moved misc legacy stuff from OldGoals to Misc_Legacy;
wenzelm
parents:
36862
diff
changeset
|
31 |
Cardinal_AC.thy Datatype_ZF.thy Epsilon.thy EquivClass.thy \ |
2fbbf0a48cef
moved misc legacy stuff from OldGoals to Misc_Legacy;
wenzelm
parents:
36862
diff
changeset
|
32 |
Finite.thy Fixedpt.thy Inductive_ZF.thy InfDatatype.thy Int_ZF.thy \ |
2fbbf0a48cef
moved misc legacy stuff from OldGoals to Misc_Legacy;
wenzelm
parents:
36862
diff
changeset
|
33 |
IntArith.thy IntDiv_ZF.thy List_ZF.thy Main.thy Main_ZF.thy \ |
2fbbf0a48cef
moved misc legacy stuff from OldGoals to Misc_Legacy;
wenzelm
parents:
36862
diff
changeset
|
34 |
Main_ZFC.thy Nat_ZF.thy OrdQuant.thy Order.thy OrderArith.thy \ |
2fbbf0a48cef
moved misc legacy stuff from OldGoals to Misc_Legacy;
wenzelm
parents:
36862
diff
changeset
|
35 |
OrderType.thy Ordinal.thy Perm.thy QPair.thy QUniv.thy ROOT.ML \ |
2fbbf0a48cef
moved misc legacy stuff from OldGoals to Misc_Legacy;
wenzelm
parents:
36862
diff
changeset
|
36 |
Sum.thy Tools/cartprod.ML Tools/datatype_package.ML \ |
2fbbf0a48cef
moved misc legacy stuff from OldGoals to Misc_Legacy;
wenzelm
parents:
36862
diff
changeset
|
37 |
Tools/ind_cases.ML Tools/induct_tacs.ML Tools/inductive_package.ML \ |
2fbbf0a48cef
moved misc legacy stuff from OldGoals to Misc_Legacy;
wenzelm
parents:
36862
diff
changeset
|
38 |
Tools/numeral_syntax.ML Tools/primrec_package.ML Tools/typechk.ML \ |
2fbbf0a48cef
moved misc legacy stuff from OldGoals to Misc_Legacy;
wenzelm
parents:
36862
diff
changeset
|
39 |
Trancl.thy Univ.thy WF.thy ZF.thy Zorn.thy arith_data.ML \ |
2fbbf0a48cef
moved misc legacy stuff from OldGoals to Misc_Legacy;
wenzelm
parents:
36862
diff
changeset
|
40 |
equalities.thy func.thy ind_syntax.ML int_arith.ML pair.thy \ |
2fbbf0a48cef
moved misc legacy stuff from OldGoals to Misc_Legacy;
wenzelm
parents:
36862
diff
changeset
|
41 |
simpdata.ML upair.thy |
28500 | 42 |
@$(ISABELLE_TOOL) usedir -b -g true -r $(OUT)/FOL ZF |
2500 | 43 |
|
44 |
||
4518 | 45 |
## ZF-AC |
2500 | 46 |
|
4518 | 47 |
ZF-AC: ZF $(LOG)/ZF-AC.gz |
2500 | 48 |
|
27203 | 49 |
$(LOG)/ZF-AC.gz: $(OUT)/ZF AC/ROOT.ML AC/AC15_WO6.thy AC/AC16_WO4.thy \ |
50 |
AC/AC16_lemmas.thy AC/AC17_AC1.thy AC/AC18_AC19.thy AC/AC7_AC9.thy \ |
|
51 |
AC/AC_Equiv.thy AC/Cardinal_aux.thy AC/DC.thy AC/HH.thy \ |
|
52 |
AC/Hartog.thy AC/WO1_AC.thy AC/WO1_WO7.thy AC/WO2_AC16.thy \ |
|
53 |
AC/WO6_WO1.thy AC/document/root.bib AC/document/root.tex |
|
28500 | 54 |
@$(ISABELLE_TOOL) usedir -g true $(OUT)/ZF AC |
2500 | 55 |
|
56 |
||
11479 | 57 |
## ZF-Coind |
4518 | 58 |
|
11479 | 59 |
ZF-Coind: ZF $(LOG)/ZF-Coind.gz |
2500 | 60 |
|
27203 | 61 |
$(LOG)/ZF-Coind.gz: $(OUT)/ZF Coind/Dynamic.thy Coind/ECR.thy \ |
62 |
Coind/Language.thy Coind/Map.thy Coind/ROOT.ML Coind/Static.thy \ |
|
63 |
Coind/Types.thy Coind/Values.thy |
|
28500 | 64 |
@$(ISABELLE_TOOL) usedir $(OUT)/ZF Coind |
2500 | 65 |
|
66 |
||
13225 | 67 |
## ZF-Constructible |
68 |
||
69 |
ZF-Constructible: ZF $(LOG)/ZF-Constructible.gz |
|
70 |
||
27203 | 71 |
$(LOG)/ZF-Constructible.gz: $(OUT)/ZF Constructible/ROOT.ML \ |
72 |
Constructible/Datatype_absolute.thy Constructible/DPow_absolute.thy \ |
|
73 |
Constructible/Formula.thy Constructible/Internalize.thy \ |
|
74 |
Constructible/AC_in_L.thy Constructible/Relative.thy \ |
|
75 |
Constructible/L_axioms.thy Constructible/Wellorderings.thy \ |
|
76 |
Constructible/MetaExists.thy Constructible/Normal.thy \ |
|
77 |
Constructible/Rank.thy Constructible/Rank_Separation.thy \ |
|
78 |
Constructible/Rec_Separation.thy Constructible/Separation.thy \ |
|
79 |
Constructible/Satisfies_absolute.thy Constructible/WF_absolute.thy \ |
|
80 |
Constructible/Reflection.thy Constructible/WFrec.thy \ |
|
15083 | 81 |
Constructible/document/root.bib Constructible/document/root.tex |
28500 | 82 |
@$(ISABELLE_TOOL) usedir -g true $(OUT)/ZF Constructible |
13225 | 83 |
|
84 |
||
11479 | 85 |
## ZF-IMP |
86 |
||
87 |
ZF-IMP: ZF $(LOG)/ZF-IMP.gz |
|
88 |
||
27203 | 89 |
$(LOG)/ZF-IMP.gz: $(OUT)/ZF IMP/Com.thy IMP/Denotation.thy \ |
90 |
IMP/Equiv.thy IMP/ROOT.ML IMP/document/root.bib \ |
|
91 |
IMP/document/root.tex |
|
28500 | 92 |
@$(ISABELLE_TOOL) usedir $(OUT)/ZF IMP |
11479 | 93 |
|
94 |
||
95 |
## ZF-Resid |
|
96 |
||
97 |
ZF-Resid: ZF $(LOG)/ZF-Resid.gz |
|
98 |
||
27203 | 99 |
$(LOG)/ZF-Resid.gz: $(OUT)/ZF Resid/ROOT.ML Resid/Confluence.thy \ |
100 |
Resid/Redex.thy Resid/Reduction.thy Resid/Residuals.thy \ |
|
101 |
Resid/Substitution.thy |
|
28500 | 102 |
@$(ISABELLE_TOOL) usedir $(OUT)/ZF Resid |
11479 | 103 |
|
104 |
||
105 |
## ZF-UNITY |
|
106 |
||
107 |
ZF-UNITY: ZF $(LOG)/ZF-UNITY.gz |
|
108 |
||
27203 | 109 |
$(LOG)/ZF-UNITY.gz: $(OUT)/ZF UNITY/ROOT.ML UNITY/Comp.thy \ |
110 |
UNITY/Constrains.thy UNITY/FP.thy UNITY/GenPrefix.thy UNITY/Guar.thy \ |
|
111 |
UNITY/Mutex.thy UNITY/State.thy UNITY/SubstAx.thy UNITY/UNITY.thy \ |
|
112 |
UNITY/Union.thy UNITY/AllocBase.thy UNITY/AllocImpl.thy \ |
|
113 |
UNITY/ClientImpl.thy UNITY/Distributor.thy UNITY/Follows.thy \ |
|
114 |
UNITY/Increasing.thy UNITY/Merge.thy UNITY/Monotonicity.thy \ |
|
115 |
UNITY/MultisetSum.thy UNITY/WFair.thy |
|
28500 | 116 |
@$(ISABELLE_TOOL) usedir $(OUT)/ZF UNITY |
11479 | 117 |
|
118 |
||
12088 | 119 |
## ZF-Induct |
120 |
||
121 |
ZF-Induct: ZF $(LOG)/ZF-Induct.gz |
|
122 |
||
27203 | 123 |
$(LOG)/ZF-Induct.gz: $(OUT)/ZF Induct/ROOT.ML Induct/Acc.thy \ |
124 |
Induct/Binary_Trees.thy Induct/Brouwer.thy Induct/Comb.thy \ |
|
125 |
Induct/Datatypes.thy Induct/FoldSet.thy Induct/ListN.thy \ |
|
126 |
Induct/Multiset.thy Induct/Mutil.thy Induct/Ntree.thy \ |
|
127 |
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
|
128 |
Induct/Term.thy Induct/Tree_Forest.thy Induct/document/root.tex |
28500 | 129 |
@$(ISABELLE_TOOL) usedir $(OUT)/ZF Induct |
12088 | 130 |
|
12175 | 131 |
|
12088 | 132 |
## ZF-ex |
133 |
||
134 |
ZF-ex: ZF $(LOG)/ZF-ex.gz |
|
135 |
||
27203 | 136 |
$(LOG)/ZF-ex.gz: $(OUT)/ZF ex/ROOT.ML ex/BinEx.thy ex/CoUnit.thy \ |
137 |
ex/Commutation.thy ex/Group.thy ex/Limit.thy ex/LList.thy \ |
|
138 |
ex/Primes.thy ex/NatSum.thy ex/Ramsey.thy ex/Ring.thy ex/misc.thy |
|
28500 | 139 |
@$(ISABELLE_TOOL) usedir $(OUT)/ZF ex |
12088 | 140 |
|
141 |
||
4518 | 142 |
## clean |
4447 | 143 |
|
144 |
clean: |
|
33450 | 145 |
@rm -f $(OUT)/ZF $(LOG)/ZF.gz $(LOG)/ZF-AC.gz \ |
146 |
$(LOG)/ZF-Coind.gz $(LOG)/ZF-Constructible.gz \ |
|
147 |
$(LOG)/ZF-ex.gz $(LOG)/ZF-IMP.gz $(LOG)/ZF-Induct.gz \ |
|
148 |
$(LOG)/ZF-Resid.gz $(LOG)/ZF-UNITY.gz |