25 ZF: FOL $(OUT)/ZF |
25 ZF: FOL $(OUT)/ZF |
26 |
26 |
27 FOL: |
27 FOL: |
28 @cd $(SRC)/FOL; $(ISABELLE_TOOL) make FOL |
28 @cd $(SRC)/FOL; $(ISABELLE_TOOL) make FOL |
29 |
29 |
30 $(OUT)/ZF: $(OUT)/FOL $(SRC)/Tools/misc_legacy.ML AC.thy Arith.thy \ |
30 $(OUT)/ZF: $(OUT)/FOL AC.thy Arith.thy ArithSimp.thy Bin.thy Bool.thy \ |
31 ArithSimp.thy Bin.thy Bool.thy Cardinal.thy CardinalArith.thy \ |
31 Cardinal.thy CardinalArith.thy Cardinal_AC.thy Datatype_ZF.thy \ |
32 Cardinal_AC.thy Datatype_ZF.thy Epsilon.thy EquivClass.thy \ |
32 Epsilon.thy EquivClass.thy Finite.thy Fixedpt.thy Inductive_ZF.thy \ |
33 Finite.thy Fixedpt.thy Inductive_ZF.thy InfDatatype.thy Int_ZF.thy \ |
33 InfDatatype.thy Int_ZF.thy IntArith.thy IntDiv_ZF.thy List_ZF.thy \ |
34 IntArith.thy IntDiv_ZF.thy List_ZF.thy Main.thy Main_ZF.thy \ |
34 Main.thy Main_ZF.thy Main_ZFC.thy Nat_ZF.thy OrdQuant.thy Order.thy \ |
35 Main_ZFC.thy Nat_ZF.thy OrdQuant.thy Order.thy OrderArith.thy \ |
35 OrderArith.thy OrderType.thy Ordinal.thy Perm.thy QPair.thy \ |
36 OrderType.thy Ordinal.thy Perm.thy QPair.thy QUniv.thy ROOT.ML \ |
36 QUniv.thy ROOT.ML Sum.thy Tools/cartprod.ML \ |
37 Sum.thy Tools/cartprod.ML Tools/datatype_package.ML \ |
37 Tools/datatype_package.ML Tools/ind_cases.ML Tools/induct_tacs.ML \ |
38 Tools/ind_cases.ML Tools/induct_tacs.ML Tools/inductive_package.ML \ |
38 Tools/inductive_package.ML Tools/numeral_syntax.ML \ |
39 Tools/numeral_syntax.ML Tools/primrec_package.ML Tools/typechk.ML \ |
39 Tools/primrec_package.ML Tools/typechk.ML Trancl.thy Univ.thy WF.thy \ |
40 Trancl.thy Univ.thy WF.thy ZF.thy Zorn.thy arith_data.ML \ |
40 ZF.thy Zorn.thy arith_data.ML equalities.thy func.thy ind_syntax.ML \ |
41 equalities.thy func.thy ind_syntax.ML int_arith.ML pair.thy \ |
41 int_arith.ML pair.thy simpdata.ML upair.thy |
42 simpdata.ML upair.thy |
|
43 @$(ISABELLE_TOOL) usedir -b -g true -r $(OUT)/FOL ZF |
42 @$(ISABELLE_TOOL) usedir -b -g true -r $(OUT)/FOL ZF |
44 |
43 |
45 |
44 |
46 ## ZF-AC |
45 ## ZF-AC |
47 |
46 |