19 BIN = $(ISABELLEBIN) |
19 BIN = $(ISABELLEBIN) |
20 COMP = $(ISABELLECOMP) |
20 COMP = $(ISABELLECOMP) |
21 FILES = ROOT.ML ZF.thy ZF.ML upair.ML subset.ML pair.ML domrange.ML \ |
21 FILES = ROOT.ML ZF.thy ZF.ML upair.ML subset.ML pair.ML domrange.ML \ |
22 func.ML AC.thy AC.ML simpdata.ML Bool.thy Bool.ML \ |
22 func.ML AC.thy AC.ML simpdata.ML Bool.thy Bool.ML \ |
23 Sum.thy Sum.ML QPair.thy QPair.ML mono.ML Fixedpt.thy Fixedpt.ML \ |
23 Sum.thy Sum.ML QPair.thy QPair.ML mono.ML Fixedpt.thy Fixedpt.ML \ |
24 ind_syntax.ML intr_elim.ML indrule.ML inductive.ML coinductive.ML \ |
24 ind_syntax.ML add_ind_def.thy add_ind_def.ML \ |
|
25 \ intr_elim.ML indrule.ML inductive.ML \ |
25 equalities.ML Perm.thy Perm.ML Rel.thy Rel.ML Trancl.thy Trancl.ML \ |
26 equalities.ML Perm.thy Perm.ML Rel.thy Rel.ML Trancl.thy Trancl.ML \ |
26 WF.thy WF.ML Order.thy Order.ML Ordinal.thy Ordinal.ML \ |
27 WF.thy WF.ML Order.thy Order.ML Ordinal.thy Ordinal.ML \ |
27 Epsilon.thy Epsilon.ML Arith.thy Arith.ML Univ.thy Univ.ML \ |
28 Epsilon.thy Epsilon.ML Arith.thy Arith.ML Univ.thy Univ.ML \ |
28 QUniv.thy QUniv.ML constructor.ML Datatype.thy Datatype.ML \ |
29 QUniv.thy QUniv.ML constructor.ML Datatype.thy Datatype.ML \ |
29 OrderArith.thy OrderArith.ML OrderType.thy OrderType.ML \ |
30 OrderArith.thy OrderArith.ML OrderType.thy OrderType.ML \ |
30 Cardinal.thy Cardinal.ML CardinalArith.thy CardinalArith.ML \ |
31 Cardinal.thy Cardinal.ML CardinalArith.thy CardinalArith.ML \ |
31 Cardinal_AC.thy Cardinal_AC.ML InfDatatype.thy InfDatatype.ML \ |
32 Cardinal_AC.thy Cardinal_AC.ML InfDatatype.thy InfDatatype.ML \ |
32 Zorn0.thy Zorn0.ML Zorn.thy Zorn.ML Nat.thy Nat.ML Fin.ML \ |
33 Zorn.thy Zorn.ML Nat.thy Nat.ML Finite.thy Finite.ML \ |
33 List.ML ListFn.thy ListFn.ML |
34 List.thy List.ML |
34 |
35 |
35 IMP_FILES = IMP/ROOT.ML IMP/Aexp.ML IMP/Aexp.thy IMP/Assign.ML IMP/Assign.thy\ |
36 IMP_FILES = IMP/ROOT.ML IMP/Com.ML IMP/Com.thy IMP/Denotation.ML\ |
36 IMP/Bexp.ML IMP/Bexp.thy IMP/Com.ML IMP/Com.thy IMP/Denotation.ML\ |
37 IMP/Denotation.thy IMP/Equiv.ML IMP/Equiv.thy |
37 IMP/Denotation.thy IMP/Equiv.ML IMP/Equiv.thy IMP/Evala0.thy\ |
|
38 IMP/Evala.ML IMP/Evala.thy IMP/Evalb0.thy IMP/Evalb.ML\ |
|
39 IMP/Evalb.thy IMP/Evalc0.thy IMP/Evalc.ML IMP/Evalc.thy |
|
40 |
38 |
41 EX_FILES = ex/ROOT.ML ex/Acc.ML ex/Bin.ML ex/BinFn.ML ex/BinFn.thy\ |
39 EX_FILES = ex/ROOT.ML ex/misc.ML ex/Ramsey.ML ex/Ramsey.thy\ |
42 ex/BT.ML ex/BT_Fn.ML ex/BT_Fn.thy ex/Comb.ML\ |
40 ex/Equiv.ML ex/Equiv.thy ex/Integ.ML ex/Integ.thy\ |
43 ex/Contract0.ML ex/Contract0.thy ex/CoUnit.ML ex/Data.ML\ |
41 ex/twos_compl.ML ex/Bin.thy ex/Bin.ML\ |
44 ex/Enum.ML ex/Equiv.ML ex/Equiv.thy ex/Integ.ML ex/Integ.thy\ |
42 ex/BT.thy ex/BT.ML ex/Term.thy ex/Term.ML \ |
45 ex/ListN.ML ex/LList.ML ex/LList_Eq.ML ex/LListFn.ML ex/LListFn.thy\ |
43 ex/TF.thy ex/TF.ML ex/Ntree.thy ex/Ntree.ML \ |
46 ex/misc.ML ex/ParContract.ML ex/Primrec0.ML ex/Primrec0.thy\ |
44 ex/Brouwer.thy ex/Brouwer.ML \ |
47 ex/Prop.ML ex/PropLog.ML ex/PropLog.thy ex/Ramsey.ML ex/Ramsey.thy\ |
45 ex/Data.thy ex/Data.ML ex/Enum.thy ex/Enum.ML \ |
48 ex/Rmap.ML ex/Term.ML ex/TermFn.ML ex/TermFn.thy \ |
46 ex/Rmap.thy ex/Rmap.ML ex/PropLog.ML ex/PropLog.thy \ |
49 ex/Ntree.ML ex/Brouwer.ML \ |
47 ex/ListN.thy ex/ListN.ML ex/Acc.thy ex/Acc.ML\ |
50 ex/TF.ML ex/TF_Fn.ML ex/TF_Fn.thy ex/twos_compl.ML |
48 ex/Comb.thy ex/Comb.ML ex/Primrec.thy ex/Primrec.ML\ |
|
49 ex/LList.thy ex/LList.ML ex/CoUnit.thy ex/CoUnit.ML |
51 |
50 |
52 #Uses cp rather than make_database because Poly/ML allows only 3 levels |
51 #Uses cp rather than make_database because Poly/ML allows only 3 levels |
53 $(BIN)/ZF: $(BIN)/FOL $(FILES) |
52 $(BIN)/ZF: $(BIN)/FOL $(FILES) |
54 case "$(COMP)" in \ |
53 case "$(COMP)" in \ |
55 poly*) cp $(BIN)/FOL $(BIN)/ZF;\ |
54 poly*) cp $(BIN)/FOL $(BIN)/ZF;\ |