21 LOG = $(OUT)/log |
21 LOG = $(OUT)/log |
22 |
22 |
23 |
23 |
24 ## ZF |
24 ## ZF |
25 |
25 |
26 ZF: FOL $(OUT)/ZF$(ML_SUFFIX) |
26 ZF: FOL $(OUT)/ZF |
27 |
27 |
28 FOL: |
28 FOL: |
29 @cd $(SRC)/FOL; $(ISATOOL) make FOL |
29 @cd $(SRC)/FOL; $(ISATOOL) make FOL |
30 |
30 |
31 $(OUT)/ZF$(ML_SUFFIX): $(OUT)/FOL$(ML_SUFFIX) AC.thy Arith.thy \ |
31 $(OUT)/ZF: $(OUT)/FOL AC.thy Arith.thy ArithSimp.thy Bin.thy Bool.thy \ |
32 ArithSimp.thy Bin.thy Bool.thy Cardinal.thy CardinalArith.thy \ |
32 Cardinal.thy CardinalArith.thy Cardinal_AC.thy Datatype_ZF.thy \ |
33 Cardinal_AC.thy Datatype_ZF.thy Epsilon.thy EquivClass.thy Finite.thy \ |
33 Epsilon.thy EquivClass.thy Finite.thy Fixedpt.thy Inductive_ZF.thy \ |
34 Fixedpt.thy Inductive_ZF.thy InfDatatype.thy Int_ZF.thy IntArith.thy \ |
34 InfDatatype.thy Int_ZF.thy IntArith.thy IntDiv_ZF.thy List_ZF.thy \ |
35 IntDiv_ZF.thy List_ZF.thy Main.thy Main_ZF.thy Main_ZFC.thy Nat_ZF.thy OrdQuant.thy \ |
35 Main.thy Main_ZF.thy Main_ZFC.thy Nat_ZF.thy OrdQuant.thy Order.thy \ |
36 Order.thy OrderArith.thy OrderType.thy Ordinal.thy Perm.thy QPair.thy \ |
36 OrderArith.thy OrderType.thy Ordinal.thy Perm.thy QPair.thy \ |
37 QUniv.thy ROOT.ML Sum.thy Tools/cartprod.ML Tools/datatype_package.ML \ |
37 QUniv.thy ROOT.ML Sum.thy Tools/cartprod.ML \ |
38 Tools/ind_cases.ML Tools/induct_tacs.ML Tools/inductive_package.ML \ |
38 Tools/datatype_package.ML Tools/ind_cases.ML Tools/induct_tacs.ML \ |
39 Tools/numeral_syntax.ML Tools/primrec_package.ML Tools/typechk.ML \ |
39 Tools/inductive_package.ML Tools/numeral_syntax.ML \ |
40 Trancl.thy Univ.thy WF.thy ZF.thy Zorn.thy arith_data.ML \ |
40 Tools/primrec_package.ML Tools/typechk.ML Trancl.thy Univ.thy WF.thy \ |
41 equalities.thy func.thy ind_syntax.ML int_arith.ML pair.thy \ |
41 ZF.thy Zorn.thy arith_data.ML equalities.thy func.thy ind_syntax.ML \ |
42 simpdata.ML upair.thy |
42 int_arith.ML pair.thy simpdata.ML upair.thy |
43 @$(ISATOOL) usedir -b -r $(OUT)/FOL ZF |
43 @$(ISATOOL) usedir -b -r $(OUT)/FOL ZF |
44 |
44 |
45 |
45 |
46 ## ZF-AC |
46 ## ZF-AC |
47 |
47 |
48 ZF-AC: ZF $(LOG)/ZF-AC.gz |
48 ZF-AC: ZF $(LOG)/ZF-AC.gz |
49 |
49 |
50 $(LOG)/ZF-AC.gz: $(OUT)/ZF$(ML_SUFFIX) \ |
50 $(LOG)/ZF-AC.gz: $(OUT)/ZF AC/ROOT.ML AC/AC15_WO6.thy AC/AC16_WO4.thy \ |
51 AC/ROOT.ML AC/AC15_WO6.thy AC/AC16_WO4.thy \ |
51 AC/AC16_lemmas.thy AC/AC17_AC1.thy AC/AC18_AC19.thy AC/AC7_AC9.thy \ |
52 AC/AC16_lemmas.thy AC/AC17_AC1.thy AC/AC18_AC19.thy AC/AC7_AC9.thy \ |
52 AC/AC_Equiv.thy AC/Cardinal_aux.thy AC/DC.thy AC/HH.thy \ |
53 AC/AC_Equiv.thy AC/Cardinal_aux.thy \ |
53 AC/Hartog.thy AC/WO1_AC.thy AC/WO1_WO7.thy AC/WO2_AC16.thy \ |
54 AC/DC.thy AC/HH.thy AC/Hartog.thy AC/WO1_AC.thy AC/WO1_WO7.thy \ |
54 AC/WO6_WO1.thy AC/document/root.bib AC/document/root.tex |
55 AC/WO2_AC16.thy AC/WO6_WO1.thy AC/document/root.bib AC/document/root.tex |
|
56 @$(ISATOOL) usedir -g true $(OUT)/ZF AC |
55 @$(ISATOOL) usedir -g true $(OUT)/ZF AC |
57 |
56 |
58 |
57 |
59 ## ZF-Coind |
58 ## ZF-Coind |
60 |
59 |
61 ZF-Coind: ZF $(LOG)/ZF-Coind.gz |
60 ZF-Coind: ZF $(LOG)/ZF-Coind.gz |
62 |
61 |
63 $(LOG)/ZF-Coind.gz: $(OUT)/ZF$(ML_SUFFIX) Coind/Dynamic.thy \ |
62 $(LOG)/ZF-Coind.gz: $(OUT)/ZF Coind/Dynamic.thy Coind/ECR.thy \ |
64 Coind/ECR.thy Coind/Language.thy Coind/Map.thy Coind/ROOT.ML \ |
63 Coind/Language.thy Coind/Map.thy Coind/ROOT.ML Coind/Static.thy \ |
65 Coind/Static.thy Coind/Types.thy Coind/Values.thy |
64 Coind/Types.thy Coind/Values.thy |
66 @$(ISATOOL) usedir $(OUT)/ZF Coind |
65 @$(ISATOOL) usedir $(OUT)/ZF Coind |
67 |
66 |
68 |
67 |
69 ## ZF-Constructible |
68 ## ZF-Constructible |
70 |
69 |
71 ZF-Constructible: ZF $(LOG)/ZF-Constructible.gz |
70 ZF-Constructible: ZF $(LOG)/ZF-Constructible.gz |
72 |
71 |
73 $(LOG)/ZF-Constructible.gz: $(OUT)/ZF$(ML_SUFFIX) Constructible/ROOT.ML \ |
72 $(LOG)/ZF-Constructible.gz: $(OUT)/ZF Constructible/ROOT.ML \ |
74 Constructible/Datatype_absolute.thy Constructible/DPow_absolute.thy\ |
73 Constructible/Datatype_absolute.thy Constructible/DPow_absolute.thy \ |
75 Constructible/Formula.thy Constructible/Internalize.thy \ |
74 Constructible/Formula.thy Constructible/Internalize.thy \ |
76 Constructible/AC_in_L.thy Constructible/Relative.thy \ |
75 Constructible/AC_in_L.thy Constructible/Relative.thy \ |
77 Constructible/L_axioms.thy Constructible/Wellorderings.thy \ |
76 Constructible/L_axioms.thy Constructible/Wellorderings.thy \ |
78 Constructible/MetaExists.thy Constructible/Normal.thy \ |
77 Constructible/MetaExists.thy Constructible/Normal.thy \ |
79 Constructible/Rank.thy Constructible/Rank_Separation.thy \ |
78 Constructible/Rank.thy Constructible/Rank_Separation.thy \ |
80 Constructible/Rec_Separation.thy Constructible/Separation.thy \ |
79 Constructible/Rec_Separation.thy Constructible/Separation.thy \ |
81 Constructible/Satisfies_absolute.thy Constructible/WF_absolute.thy \ |
80 Constructible/Satisfies_absolute.thy Constructible/WF_absolute.thy \ |
82 Constructible/Reflection.thy Constructible/WFrec.thy \ |
81 Constructible/Reflection.thy Constructible/WFrec.thy \ |
83 Constructible/document/root.bib Constructible/document/root.tex |
82 Constructible/document/root.bib Constructible/document/root.tex |
84 @$(ISATOOL) usedir -g true $(OUT)/ZF Constructible |
83 @$(ISATOOL) usedir -g true $(OUT)/ZF Constructible |
85 |
84 |
86 |
85 |
87 ## ZF-IMP |
86 ## ZF-IMP |
88 |
87 |
89 ZF-IMP: ZF $(LOG)/ZF-IMP.gz |
88 ZF-IMP: ZF $(LOG)/ZF-IMP.gz |
90 |
89 |
91 $(LOG)/ZF-IMP.gz: $(OUT)/ZF$(ML_SUFFIX) IMP/Com.thy IMP/Denotation.thy IMP/Equiv.thy \ |
90 $(LOG)/ZF-IMP.gz: $(OUT)/ZF IMP/Com.thy IMP/Denotation.thy \ |
92 IMP/ROOT.ML IMP/document/root.bib IMP/document/root.tex |
91 IMP/Equiv.thy IMP/ROOT.ML IMP/document/root.bib \ |
|
92 IMP/document/root.tex |
93 @$(ISATOOL) usedir $(OUT)/ZF IMP |
93 @$(ISATOOL) usedir $(OUT)/ZF IMP |
94 |
94 |
95 |
95 |
96 ## ZF-Resid |
96 ## ZF-Resid |
97 |
97 |
98 ZF-Resid: ZF $(LOG)/ZF-Resid.gz |
98 ZF-Resid: ZF $(LOG)/ZF-Resid.gz |
99 |
99 |
100 $(LOG)/ZF-Resid.gz: $(OUT)/ZF$(ML_SUFFIX) Resid/ROOT.ML \ |
100 $(LOG)/ZF-Resid.gz: $(OUT)/ZF Resid/ROOT.ML Resid/Confluence.thy \ |
101 Resid/Confluence.thy Resid/Redex.thy \ |
101 Resid/Redex.thy Resid/Reduction.thy Resid/Residuals.thy \ |
102 Resid/Reduction.thy Resid/Residuals.thy Resid/Substitution.thy |
102 Resid/Substitution.thy |
103 @$(ISATOOL) usedir $(OUT)/ZF Resid |
103 @$(ISATOOL) usedir $(OUT)/ZF Resid |
104 |
104 |
105 |
105 |
106 ## ZF-UNITY |
106 ## ZF-UNITY |
107 |
107 |
108 ZF-UNITY: ZF $(LOG)/ZF-UNITY.gz |
108 ZF-UNITY: ZF $(LOG)/ZF-UNITY.gz |
109 |
109 |
110 $(LOG)/ZF-UNITY.gz: $(OUT)/ZF$(ML_SUFFIX) UNITY/ROOT.ML \ |
110 $(LOG)/ZF-UNITY.gz: $(OUT)/ZF UNITY/ROOT.ML UNITY/Comp.thy \ |
111 UNITY/Comp.thy UNITY/Constrains.thy UNITY/FP.thy\ |
111 UNITY/Constrains.thy UNITY/FP.thy UNITY/GenPrefix.thy UNITY/Guar.thy \ |
112 UNITY/GenPrefix.thy UNITY/Guar.thy UNITY/Mutex.thy UNITY/State.thy \ |
112 UNITY/Mutex.thy UNITY/State.thy UNITY/SubstAx.thy UNITY/UNITY.thy \ |
113 UNITY/SubstAx.thy UNITY/UNITY.thy UNITY/Union.thy \ |
113 UNITY/Union.thy UNITY/AllocBase.thy UNITY/AllocImpl.thy \ |
114 UNITY/AllocBase.thy UNITY/AllocImpl.thy\ |
114 UNITY/ClientImpl.thy UNITY/Distributor.thy UNITY/Follows.thy \ |
115 UNITY/ClientImpl.thy UNITY/Distributor.thy\ |
115 UNITY/Increasing.thy UNITY/Merge.thy UNITY/Monotonicity.thy \ |
116 UNITY/Follows.thy UNITY/Increasing.thy UNITY/Merge.thy\ |
116 UNITY/MultisetSum.thy UNITY/WFair.thy |
117 UNITY/Monotonicity.thy UNITY/MultisetSum.thy UNITY/WFair.thy |
|
118 @$(ISATOOL) usedir $(OUT)/ZF UNITY |
117 @$(ISATOOL) usedir $(OUT)/ZF UNITY |
119 |
118 |
120 |
119 |
121 ## ZF-Induct |
120 ## ZF-Induct |
122 |
121 |
123 ZF-Induct: ZF $(LOG)/ZF-Induct.gz |
122 ZF-Induct: ZF $(LOG)/ZF-Induct.gz |
124 |
123 |
125 $(LOG)/ZF-Induct.gz: $(OUT)/ZF$(ML_SUFFIX) Induct/ROOT.ML Induct/Acc.thy \ |
124 $(LOG)/ZF-Induct.gz: $(OUT)/ZF Induct/ROOT.ML Induct/Acc.thy \ |
126 Induct/Binary_Trees.thy Induct/Brouwer.thy Induct/Comb.thy \ |
125 Induct/Binary_Trees.thy Induct/Brouwer.thy Induct/Comb.thy \ |
127 Induct/Datatypes.thy Induct/FoldSet.thy \ |
126 Induct/Datatypes.thy Induct/FoldSet.thy Induct/ListN.thy \ |
128 Induct/ListN.thy Induct/Multiset.thy Induct/Mutil.thy \ |
127 Induct/Multiset.thy Induct/Mutil.thy Induct/Ntree.thy \ |
129 Induct/Ntree.thy Induct/Primrec.thy Induct/PropLog.thy Induct/Rmap.thy \ |
128 Induct/Primrec.thy Induct/PropLog.thy Induct/Rmap.thy \ |
130 Induct/Term.thy Induct/Tree_Forest.thy Induct/document/root.tex |
129 Induct/Term.thy Induct/Tree_Forest.thy Induct/document/root.tex |
131 @$(ISATOOL) usedir $(OUT)/ZF Induct |
130 @$(ISATOOL) usedir $(OUT)/ZF Induct |
132 |
131 |
133 |
132 |
134 ## ZF-ex |
133 ## ZF-ex |
135 |
134 |
136 ZF-ex: ZF $(LOG)/ZF-ex.gz |
135 ZF-ex: ZF $(LOG)/ZF-ex.gz |
137 |
136 |
138 $(LOG)/ZF-ex.gz: $(OUT)/ZF$(ML_SUFFIX) ex/ROOT.ML \ |
137 $(LOG)/ZF-ex.gz: $(OUT)/ZF ex/ROOT.ML ex/BinEx.thy ex/CoUnit.thy \ |
139 ex/BinEx.thy ex/CoUnit.thy ex/Commutation.thy ex/Group.thy\ |
138 ex/Commutation.thy ex/Group.thy ex/Limit.thy ex/LList.thy \ |
140 ex/Limit.thy ex/LList.thy ex/Primes.thy \ |
139 ex/Primes.thy ex/NatSum.thy ex/Ramsey.thy ex/Ring.thy ex/misc.thy |
141 ex/NatSum.thy ex/Ramsey.thy ex/Ring.thy ex/misc.thy |
|
142 @$(ISATOOL) usedir $(OUT)/ZF ex |
140 @$(ISATOOL) usedir $(OUT)/ZF ex |
143 |
141 |
144 |
142 |
145 ## clean |
143 ## clean |
146 |
144 |
147 clean: |
145 clean: |
148 @rm -f $(OUT)/ZF$(ML_SUFFIX) $(LOG)/ZF.gz $(LOG)/ZF-AC.gz $(LOG)/ZF-Coind.gz \ |
146 @rm -f $(OUT)/ZF $(LOG)/ZF.gz $(LOG)/ZF-AC.gz $(LOG)/ZF-Coind.gz \ |
149 $(LOG)/ZF-Constructible.gz $(LOG)/ZF-ex.gz \ |
147 $(LOG)/ZF-Constructible.gz $(LOG)/ZF-ex.gz \ |
150 $(LOG)/ZF-IMP.gz $(LOG)/ZF-Resid.gz \ |
148 $(LOG)/ZF-IMP.gz $(LOG)/ZF-Resid.gz \ |
151 $(LOG)/ZF-UNITY.gz |
149 $(LOG)/ZF-UNITY.gz |