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; $(ISATOOL) make FOL |
30 |
30 |
31 $(OUT)/ZF: $(OUT)/FOL AC.ML AC.thy Arith.ML Arith.thy Bool.ML \ |
31 $(OUT)/ZF: $(OUT)/FOL AC.ML AC.thy Arith.ML Arith.thy ArithSimp.ML \ |
32 arith_data.ML ArithSimp.thy ArithSimp.ML Bool.thy \ |
32 ArithSimp.thy Bool.ML Bool.thy Cardinal.ML Cardinal.thy \ |
33 Cardinal.ML Cardinal.thy CardinalArith.ML CardinalArith.thy \ |
33 CardinalArith.ML CardinalArith.thy Cardinal_AC.ML Cardinal_AC.thy \ |
34 Cardinal_AC.ML Cardinal_AC.thy Datatype.ML Datatype.thy Epsilon.ML \ |
34 Datatype.ML Datatype.thy Epsilon.ML Epsilon.thy Finite.ML Finite.thy \ |
35 Epsilon.thy Finite.ML Finite.thy Fixedpt.ML Fixedpt.thy Inductive.ML \ |
35 Fixedpt.ML Fixedpt.thy Inductive.ML Inductive.thy InfDatatype.ML \ |
36 Inductive.thy InfDatatype.ML InfDatatype.thy \ |
36 InfDatatype.thy Integ/Bin.ML Integ/Bin.thy Integ/EquivClass.ML \ |
37 Integ/Bin.ML Integ/Bin.thy \ |
37 Integ/EquivClass.thy Integ/Int.ML Integ/Int.thy Integ/IntArith.thy \ |
38 Integ/EquivClass.ML Integ/EquivClass.thy Integ/Int.ML Integ/Int.thy \ |
38 Integ/IntDiv.ML Integ/IntDiv.thy Integ/int_arith.ML \ |
39 Integ/IntDiv.ML Integ/IntDiv.thy \ |
39 Integ/twos_compl.ML Let.ML Let.thy List.ML List.thy Main.ML Main.thy \ |
40 Integ/twos_compl.ML Integ/int_arith.ML Integ/IntArith.thy \ |
40 Nat.ML Nat.thy Order.ML Order.thy OrderArith.ML OrderArith.thy \ |
41 Let.ML Let.thy List.ML List.thy \ |
41 OrderType.ML OrderType.thy Ordinal.ML Ordinal.thy Perm.ML Perm.thy \ |
42 Main.thy Nat.ML Nat.thy Order.ML Order.thy OrderArith.ML \ |
42 QPair.ML QPair.thy QUniv.ML QUniv.thy ROOT.ML Rel.ML Rel.thy Sum.ML \ |
43 OrderArith.thy OrderType.ML OrderType.thy Ordinal.ML Ordinal.thy \ |
43 Sum.thy Tools/cartprod.ML Tools/datatype_package.ML \ |
44 Perm.ML Perm.thy QPair.ML QPair.thy QUniv.ML QUniv.thy ROOT.ML \ |
44 Tools/ind_cases.ML Tools/induct_tacs.ML Tools/inductive_package.ML \ |
45 Rel.ML Rel.thy Sum.ML Sum.thy \ |
45 Tools/numeral_syntax.ML Tools/primrec_package.ML Tools/typechk.ML \ |
46 Tools/numeral_syntax.ML Tools/cartprod.ML \ |
|
47 Tools/datatype_package.ML Tools/ind_cases.ML Tools/induct_tacs.ML \ |
|
48 Tools/inductive_package.ML Tools/primrec_package.ML Tools/typechk.ML \ |
|
49 Trancl.ML Trancl.thy Univ.ML Univ.thy Update.ML Update.thy WF.ML \ |
46 Trancl.ML Trancl.thy Univ.ML Univ.thy Update.ML Update.thy WF.ML \ |
50 WF.thy ZF.ML ZF.thy Zorn.ML Zorn.thy domrange.ML domrange.thy \ |
47 WF.thy ZF.ML ZF.thy Zorn.ML Zorn.thy arith_data.ML domrange.ML \ |
51 equalities.ML equalities.thy func.ML func.thy ind_syntax.ML mono.ML \ |
48 domrange.thy equalities.ML equalities.thy func.ML func.thy \ |
52 mono.thy pair.ML pair.thy simpdata.ML subset.ML subset.thy \ |
49 ind_syntax.ML mono.ML mono.thy pair.ML pair.thy simpdata.ML \ |
53 thy_syntax.ML upair.ML upair.thy |
50 subset.ML subset.thy thy_syntax.ML upair.ML upair.thy |
54 @$(ISATOOL) usedir -b -r $(OUT)/FOL ZF |
51 @$(ISATOOL) usedir -b -r $(OUT)/FOL ZF |
55 |
52 |
56 |
53 |
57 ## ZF-AC |
54 ## ZF-AC |
58 |
55 |