24 ## ZF |
24 ## ZF |
25 |
25 |
26 ZF: FOL $(OUT)/ZF |
26 ZF: FOL $(OUT)/ZF |
27 |
27 |
28 FOL: |
28 FOL: |
29 @cd $(SRC)/FOL; $(ISATOOL) make FOL |
29 @cd $(SRC)/FOL; $(ISABELLE_TOOL) make FOL |
30 |
30 |
31 $(OUT)/ZF: $(OUT)/FOL AC.thy Arith.thy ArithSimp.thy Bin.thy Bool.thy \ |
31 $(OUT)/ZF: $(OUT)/FOL AC.thy Arith.thy ArithSimp.thy Bin.thy Bool.thy \ |
32 Cardinal.thy CardinalArith.thy Cardinal_AC.thy Datatype_ZF.thy \ |
32 Cardinal.thy CardinalArith.thy Cardinal_AC.thy Datatype_ZF.thy \ |
33 Epsilon.thy EquivClass.thy Finite.thy Fixedpt.thy Inductive_ZF.thy \ |
33 Epsilon.thy EquivClass.thy Finite.thy Fixedpt.thy Inductive_ZF.thy \ |
34 InfDatatype.thy Int_ZF.thy IntArith.thy IntDiv_ZF.thy List_ZF.thy \ |
34 InfDatatype.thy Int_ZF.thy IntArith.thy IntDiv_ZF.thy List_ZF.thy \ |
38 Tools/datatype_package.ML Tools/ind_cases.ML Tools/induct_tacs.ML \ |
38 Tools/datatype_package.ML Tools/ind_cases.ML Tools/induct_tacs.ML \ |
39 Tools/inductive_package.ML Tools/numeral_syntax.ML \ |
39 Tools/inductive_package.ML Tools/numeral_syntax.ML \ |
40 Tools/primrec_package.ML Tools/typechk.ML Trancl.thy Univ.thy WF.thy \ |
40 Tools/primrec_package.ML Tools/typechk.ML Trancl.thy Univ.thy WF.thy \ |
41 ZF.thy Zorn.thy arith_data.ML equalities.thy func.thy ind_syntax.ML \ |
41 ZF.thy Zorn.thy arith_data.ML equalities.thy func.thy ind_syntax.ML \ |
42 int_arith.ML pair.thy simpdata.ML upair.thy |
42 int_arith.ML pair.thy simpdata.ML upair.thy |
43 @$(ISATOOL) usedir -b -g true -r $(OUT)/FOL ZF |
43 @$(ISABELLE_TOOL) usedir -b -g true -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 |
50 $(LOG)/ZF-AC.gz: $(OUT)/ZF AC/ROOT.ML AC/AC15_WO6.thy AC/AC16_WO4.thy \ |
50 $(LOG)/ZF-AC.gz: $(OUT)/ZF 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 \ |
51 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 \ |
52 AC/AC_Equiv.thy AC/Cardinal_aux.thy AC/DC.thy AC/HH.thy \ |
53 AC/Hartog.thy AC/WO1_AC.thy AC/WO1_WO7.thy AC/WO2_AC16.thy \ |
53 AC/Hartog.thy AC/WO1_AC.thy AC/WO1_WO7.thy AC/WO2_AC16.thy \ |
54 AC/WO6_WO1.thy AC/document/root.bib AC/document/root.tex |
54 AC/WO6_WO1.thy AC/document/root.bib AC/document/root.tex |
55 @$(ISATOOL) usedir -g true $(OUT)/ZF AC |
55 @$(ISABELLE_TOOL) usedir -g true $(OUT)/ZF AC |
56 |
56 |
57 |
57 |
58 ## ZF-Coind |
58 ## ZF-Coind |
59 |
59 |
60 ZF-Coind: ZF $(LOG)/ZF-Coind.gz |
60 ZF-Coind: ZF $(LOG)/ZF-Coind.gz |
61 |
61 |
62 $(LOG)/ZF-Coind.gz: $(OUT)/ZF Coind/Dynamic.thy Coind/ECR.thy \ |
62 $(LOG)/ZF-Coind.gz: $(OUT)/ZF Coind/Dynamic.thy Coind/ECR.thy \ |
63 Coind/Language.thy Coind/Map.thy Coind/ROOT.ML Coind/Static.thy \ |
63 Coind/Language.thy Coind/Map.thy Coind/ROOT.ML Coind/Static.thy \ |
64 Coind/Types.thy Coind/Values.thy |
64 Coind/Types.thy Coind/Values.thy |
65 @$(ISATOOL) usedir $(OUT)/ZF Coind |
65 @$(ISABELLE_TOOL) usedir $(OUT)/ZF Coind |
66 |
66 |
67 |
67 |
68 ## ZF-Constructible |
68 ## ZF-Constructible |
69 |
69 |
70 ZF-Constructible: ZF $(LOG)/ZF-Constructible.gz |
70 ZF-Constructible: ZF $(LOG)/ZF-Constructible.gz |
78 Constructible/Rank.thy Constructible/Rank_Separation.thy \ |
78 Constructible/Rank.thy Constructible/Rank_Separation.thy \ |
79 Constructible/Rec_Separation.thy Constructible/Separation.thy \ |
79 Constructible/Rec_Separation.thy Constructible/Separation.thy \ |
80 Constructible/Satisfies_absolute.thy Constructible/WF_absolute.thy \ |
80 Constructible/Satisfies_absolute.thy Constructible/WF_absolute.thy \ |
81 Constructible/Reflection.thy Constructible/WFrec.thy \ |
81 Constructible/Reflection.thy Constructible/WFrec.thy \ |
82 Constructible/document/root.bib Constructible/document/root.tex |
82 Constructible/document/root.bib Constructible/document/root.tex |
83 @$(ISATOOL) usedir -g true $(OUT)/ZF Constructible |
83 @$(ISABELLE_TOOL) usedir -g true $(OUT)/ZF Constructible |
84 |
84 |
85 |
85 |
86 ## ZF-IMP |
86 ## ZF-IMP |
87 |
87 |
88 ZF-IMP: ZF $(LOG)/ZF-IMP.gz |
88 ZF-IMP: ZF $(LOG)/ZF-IMP.gz |
89 |
89 |
90 $(LOG)/ZF-IMP.gz: $(OUT)/ZF IMP/Com.thy IMP/Denotation.thy \ |
90 $(LOG)/ZF-IMP.gz: $(OUT)/ZF IMP/Com.thy IMP/Denotation.thy \ |
91 IMP/Equiv.thy IMP/ROOT.ML IMP/document/root.bib \ |
91 IMP/Equiv.thy IMP/ROOT.ML IMP/document/root.bib \ |
92 IMP/document/root.tex |
92 IMP/document/root.tex |
93 @$(ISATOOL) usedir $(OUT)/ZF IMP |
93 @$(ISABELLE_TOOL) 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 Resid/ROOT.ML Resid/Confluence.thy \ |
100 $(LOG)/ZF-Resid.gz: $(OUT)/ZF Resid/ROOT.ML Resid/Confluence.thy \ |
101 Resid/Redex.thy Resid/Reduction.thy Resid/Residuals.thy \ |
101 Resid/Redex.thy Resid/Reduction.thy Resid/Residuals.thy \ |
102 Resid/Substitution.thy |
102 Resid/Substitution.thy |
103 @$(ISATOOL) usedir $(OUT)/ZF Resid |
103 @$(ISABELLE_TOOL) 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 |
112 UNITY/Mutex.thy UNITY/State.thy UNITY/SubstAx.thy UNITY/UNITY.thy \ |
112 UNITY/Mutex.thy UNITY/State.thy UNITY/SubstAx.thy UNITY/UNITY.thy \ |
113 UNITY/Union.thy UNITY/AllocBase.thy UNITY/AllocImpl.thy \ |
113 UNITY/Union.thy UNITY/AllocBase.thy UNITY/AllocImpl.thy \ |
114 UNITY/ClientImpl.thy UNITY/Distributor.thy UNITY/Follows.thy \ |
114 UNITY/ClientImpl.thy UNITY/Distributor.thy UNITY/Follows.thy \ |
115 UNITY/Increasing.thy UNITY/Merge.thy UNITY/Monotonicity.thy \ |
115 UNITY/Increasing.thy UNITY/Merge.thy UNITY/Monotonicity.thy \ |
116 UNITY/MultisetSum.thy UNITY/WFair.thy |
116 UNITY/MultisetSum.thy UNITY/WFair.thy |
117 @$(ISATOOL) usedir $(OUT)/ZF UNITY |
117 @$(ISABELLE_TOOL) usedir $(OUT)/ZF UNITY |
118 |
118 |
119 |
119 |
120 ## ZF-Induct |
120 ## ZF-Induct |
121 |
121 |
122 ZF-Induct: ZF $(LOG)/ZF-Induct.gz |
122 ZF-Induct: ZF $(LOG)/ZF-Induct.gz |
125 Induct/Binary_Trees.thy Induct/Brouwer.thy Induct/Comb.thy \ |
125 Induct/Binary_Trees.thy Induct/Brouwer.thy Induct/Comb.thy \ |
126 Induct/Datatypes.thy Induct/FoldSet.thy Induct/ListN.thy \ |
126 Induct/Datatypes.thy Induct/FoldSet.thy Induct/ListN.thy \ |
127 Induct/Multiset.thy Induct/Mutil.thy Induct/Ntree.thy \ |
127 Induct/Multiset.thy Induct/Mutil.thy Induct/Ntree.thy \ |
128 Induct/Primrec.thy Induct/PropLog.thy Induct/Rmap.thy \ |
128 Induct/Primrec.thy Induct/PropLog.thy Induct/Rmap.thy \ |
129 Induct/Term.thy Induct/Tree_Forest.thy Induct/document/root.tex |
129 Induct/Term.thy Induct/Tree_Forest.thy Induct/document/root.tex |
130 @$(ISATOOL) usedir $(OUT)/ZF Induct |
130 @$(ISABELLE_TOOL) usedir $(OUT)/ZF Induct |
131 |
131 |
132 |
132 |
133 ## ZF-ex |
133 ## ZF-ex |
134 |
134 |
135 ZF-ex: ZF $(LOG)/ZF-ex.gz |
135 ZF-ex: ZF $(LOG)/ZF-ex.gz |
136 |
136 |
137 $(LOG)/ZF-ex.gz: $(OUT)/ZF ex/ROOT.ML ex/BinEx.thy ex/CoUnit.thy \ |
137 $(LOG)/ZF-ex.gz: $(OUT)/ZF ex/ROOT.ML ex/BinEx.thy ex/CoUnit.thy \ |
138 ex/Commutation.thy ex/Group.thy ex/Limit.thy ex/LList.thy \ |
138 ex/Commutation.thy ex/Group.thy ex/Limit.thy ex/LList.thy \ |
139 ex/Primes.thy ex/NatSum.thy ex/Ramsey.thy ex/Ring.thy ex/misc.thy |
139 ex/Primes.thy ex/NatSum.thy ex/Ramsey.thy ex/Ring.thy ex/misc.thy |
140 @$(ISATOOL) usedir $(OUT)/ZF ex |
140 @$(ISABELLE_TOOL) usedir $(OUT)/ZF ex |
141 |
141 |
142 |
142 |
143 ## clean |
143 ## clean |
144 |
144 |
145 clean: |
145 clean: |