equal
deleted
inserted
replaced
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$(ML_SUFFIX): $(OUT)/FOL$(ML_SUFFIX) AC.thy Arith.thy \ |
32 ArithSimp.thy Bin.thy Bool.thy Cardinal.thy CardinalArith.thy \ |
32 ArithSimp.thy Bin.thy Bool.thy Cardinal.thy CardinalArith.thy \ |
33 Cardinal_AC.thy Datatype.thy Epsilon.thy EquivClass.thy Finite.thy \ |
33 Cardinal_AC.thy Datatype_ZF.thy Epsilon.thy EquivClass.thy Finite.thy \ |
34 Fixedpt.thy Inductive.thy InfDatatype.thy Int.thy IntArith.thy \ |
34 Fixedpt.thy Inductive_ZF.thy InfDatatype.thy Int_ZF.thy IntArith.thy \ |
35 IntDiv.thy List.thy Main.thy Main_ZFC.thy Nat.thy OrdQuant.thy \ |
35 IntDiv_ZF.thy List_ZF.thy Main.thy Main_ZF.thy Main_ZFC.thy Nat_ZF.thy OrdQuant.thy \ |
36 Order.thy OrderArith.thy OrderType.thy Ordinal.thy Perm.thy QPair.thy \ |
36 Order.thy 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 Tools/datatype_package.ML \ |
38 Tools/ind_cases.ML Tools/induct_tacs.ML Tools/inductive_package.ML \ |
38 Tools/ind_cases.ML Tools/induct_tacs.ML Tools/inductive_package.ML \ |
39 Tools/numeral_syntax.ML Tools/primrec_package.ML Tools/typechk.ML \ |
39 Tools/numeral_syntax.ML Tools/primrec_package.ML Tools/typechk.ML \ |
40 Trancl.thy Univ.thy WF.thy ZF.thy Zorn.thy arith_data.ML \ |
40 Trancl.thy Univ.thy WF.thy ZF.thy Zorn.thy arith_data.ML \ |