equal
deleted
inserted
replaced
27 @cd $(SRC)/FOL; $(ISATOOL) make FOL |
27 @cd $(SRC)/FOL; $(ISATOOL) make FOL |
28 |
28 |
29 $(OUT)/ZF: $(OUT)/FOL $(SRC)/Pure/section_utils.ML AC.ML AC.thy \ |
29 $(OUT)/ZF: $(OUT)/FOL $(SRC)/Pure/section_utils.ML AC.ML AC.thy \ |
30 Arith.ML Arith.thy Bool.ML Bool.thy Cardinal.ML Cardinal.thy \ |
30 Arith.ML Arith.thy Bool.ML Bool.thy Cardinal.ML Cardinal.thy \ |
31 CardinalArith.ML CardinalArith.thy Cardinal_AC.ML Cardinal_AC.thy \ |
31 CardinalArith.ML CardinalArith.thy Cardinal_AC.ML Cardinal_AC.thy \ |
32 Datatype.ML Datatype.thy Epsilon.ML Epsilon.thy EquivClass.ML \ |
32 Datatype.ML Datatype.thy Epsilon.ML Epsilon.thy \ |
33 EquivClass.thy Finite.ML Finite.thy Fixedpt.ML Fixedpt.thy \ |
33 Finite.ML Finite.thy Fixedpt.ML Fixedpt.thy \ |
34 Inductive.ML Inductive.thy InfDatatype.ML InfDatatype.thy \ |
34 Inductive.ML Inductive.thy InfDatatype.ML InfDatatype.thy \ |
35 Let.ML Let.thy List.ML List.thy Main.thy Nat.ML Nat.thy \ |
35 Let.ML Let.thy List.ML List.thy Main.thy Nat.ML Nat.thy \ |
36 Order.ML Order.thy OrderArith.ML \ |
36 Order.ML Order.thy OrderArith.ML \ |
37 OrderArith.thy OrderType.ML OrderType.thy Ordinal.ML Ordinal.thy \ |
37 OrderArith.thy OrderType.ML OrderType.thy Ordinal.ML Ordinal.thy \ |
38 Perm.ML Perm.thy QPair.ML QPair.thy QUniv.ML QUniv.thy ROOT.ML Rel.ML \ |
38 Perm.ML Perm.thy QPair.ML QPair.thy QUniv.ML QUniv.thy ROOT.ML Rel.ML \ |
41 ZF.ML ZF.thy Zorn.ML Zorn.thy add_ind_def.ML add_ind_def.thy \ |
41 ZF.ML ZF.thy Zorn.ML Zorn.thy add_ind_def.ML add_ind_def.thy \ |
42 cartprod.ML cartprod.thy constructor.ML constructor.thy domrange.ML \ |
42 cartprod.ML cartprod.thy constructor.ML constructor.thy domrange.ML \ |
43 domrange.thy equalities.ML equalities.thy func.ML func.thy \ |
43 domrange.thy equalities.ML equalities.thy func.ML func.thy \ |
44 ind_syntax.ML ind_syntax.thy indrule.ML indrule.thy intr_elim.ML \ |
44 ind_syntax.ML ind_syntax.thy indrule.ML indrule.thy intr_elim.ML \ |
45 intr_elim.thy mono.ML mono.thy pair.ML pair.thy simpdata.ML subset.ML \ |
45 intr_elim.thy mono.ML mono.thy pair.ML pair.thy simpdata.ML subset.ML \ |
46 subset.thy thy_syntax.ML typechk.ML upair.ML upair.thy |
46 subset.thy thy_syntax.ML typechk.ML upair.ML upair.thy \ |
|
47 Integ/EquivClass.ML Integ/EquivClass.thy Integ/Integ.ML Integ/Integ.thy \ |
|
48 Integ/twos_compl.ML Integ/Bin.ML Integ/Bin.thy |
47 @$(ISATOOL) usedir -b $(OUT)/FOL ZF |
49 @$(ISATOOL) usedir -b $(OUT)/FOL ZF |
48 |
50 |
49 |
51 |
50 ## ZF-IMP |
52 ## ZF-IMP |
51 |
53 |
102 ## ZF-ex |
104 ## ZF-ex |
103 |
105 |
104 ZF-ex: ZF $(LOG)/ZF-ex.gz |
106 ZF-ex: ZF $(LOG)/ZF-ex.gz |
105 |
107 |
106 $(LOG)/ZF-ex.gz: $(OUT)/ZF ex/Acc.ML ex/Acc.thy ex/BT.ML ex/BT.thy \ |
108 $(LOG)/ZF-ex.gz: $(OUT)/ZF ex/Acc.ML ex/Acc.thy ex/BT.ML ex/BT.thy \ |
107 ex/Bin.ML ex/Bin.thy ex/Brouwer.ML ex/Brouwer.thy ex/CoUnit.ML \ |
109 ex/BinEx.ML ex/Brouwer.ML ex/Brouwer.thy ex/CoUnit.ML \ |
108 ex/CoUnit.thy ex/Comb.ML ex/Comb.thy ex/Data.ML ex/Data.thy ex/Enum.ML \ |
110 ex/CoUnit.thy ex/Comb.ML ex/Comb.thy ex/Data.ML ex/Data.thy ex/Enum.ML \ |
109 ex/Enum.thy ex/Integ.ML ex/Integ.thy ex/LList.ML ex/LList.thy \ |
111 ex/Enum.thy ex/LList.ML ex/LList.thy \ |
110 ex/Limit.ML ex/Limit.thy ex/ListN.ML ex/ListN.thy ex/Mutil.ML \ |
112 ex/Limit.ML ex/Limit.thy ex/ListN.ML ex/ListN.thy ex/Mutil.ML \ |
111 ex/Mutil.thy ex/Ntree.ML ex/Ntree.thy ex/Primes.ML ex/Primes.thy \ |
113 ex/Mutil.thy ex/Ntree.ML ex/Ntree.thy ex/Primes.ML ex/Primes.thy \ |
112 ex/Primrec.ML ex/Primrec.thy ex/PropLog.ML ex/PropLog.thy ex/ROOT.ML \ |
114 ex/Primrec.ML ex/Primrec.thy ex/PropLog.ML ex/PropLog.thy ex/ROOT.ML \ |
113 ex/Ramsey.ML ex/Ramsey.thy ex/Rmap.ML ex/Rmap.thy ex/TF.ML ex/TF.thy \ |
115 ex/Ramsey.ML ex/Ramsey.thy ex/Rmap.ML ex/Rmap.thy ex/TF.ML ex/TF.thy \ |
114 ex/Term.ML ex/Term.thy ex/misc.ML ex/twos_compl.ML ex/twos_compl.thy |
116 ex/Term.ML ex/Term.thy ex/misc.ML |
115 @$(ISATOOL) usedir $(OUT)/ZF ex |
117 @$(ISATOOL) usedir $(OUT)/ZF ex |
116 |
118 |
117 |
119 |
118 ## clean |
120 ## clean |
119 |
121 |