18 |
18 |
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 simpdata.ML Bool.thy Bool.ML \ |
22 func.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 intr_elim.ML indrule.ML inductive.ML coinductive.ML \ |
25 equalities.ML Perm.thy Perm.ML Trancl.thy Trancl.ML \ |
25 equalities.ML Perm.thy Perm.ML Trancl.thy Trancl.ML \ |
26 WF.thy WF.ML Ord.thy Ord.ML Nat.thy Nat.ML \ |
26 WF.thy WF.ML Ord.thy Ord.ML Nat.thy Nat.ML \ |
27 Epsilon.thy Epsilon.ML Arith.thy Arith.ML Univ.thy Univ.ML \ |
27 Epsilon.thy Epsilon.ML Arith.thy Arith.ML Univ.thy Univ.ML \ |
28 Quniv.thy Quniv.ML constructor.ML datatype.ML \ |
28 QUniv.thy QUniv.ML constructor.ML Datatype.ML \ |
29 fin.ML list.ML ListFn.thy ListFn.ML |
29 fin.ML List.ML ListFn.thy ListFn.ML |
30 |
30 |
31 EX_FILES = ex/ROOT.ML ex/acc.ML ex/bin.ML ex/BinFn.ML ex/BinFn.thy\ |
31 EX_FILES = ex/ROOT.ML ex/Acc.ML ex/Bin.ML ex/BinFn.ML ex/BinFn.thy\ |
32 ex/BT.ML ex/BT_Fn.ML ex/BT_Fn.thy ex/comb.ML\ |
32 ex/BT.ML ex/BT_Fn.ML ex/BT_Fn.thy ex/Comb.ML\ |
33 ex/Contract0.ML ex/Contract0.thy ex/counit.ML ex/data.ML\ |
33 ex/Contract0.ML ex/Contract0.thy ex/counit.ML ex/Data.ML\ |
34 ex/enum.ML ex/Equiv.ML ex/Equiv.thy ex/Integ.ML ex/Integ.thy\ |
34 ex/Enum.ML ex/Equiv.ML ex/Equiv.thy ex/Integ.ML ex/Integ.thy\ |
35 ex/listn.ML ex/llist.ML ex/llist_eq.ML ex/LListFn.ML ex/LListFn.thy\ |
35 ex/ListN.ML ex/llist.ML ex/LList_Eq.ML ex/LListFn.ML ex/LListFn.thy\ |
36 ex/misc.ML ex/parcontract.ML ex/Primrec0.ML ex/Primrec0.thy\ |
36 ex/misc.ML ex/ParContract.ML ex/Primrec0.ML ex/Primrec0.thy\ |
37 ex/prop.ML ex/PropLog.ML ex/PropLog.thy ex/Ramsey.ML ex/Ramsey.thy\ |
37 ex/Prop.ML ex/PropLog.ML ex/PropLog.thy ex/Ramsey.ML ex/Ramsey.thy\ |
38 ex/rmap.ML ex/term.ML ex/TermFn.ML ex/TermFn.thy ex/tf.ML\ |
38 ex/Rmap.ML ex/Term.ML ex/TermFn.ML ex/TermFn.thy ex/TF.ML\ |
39 ex/TF_Fn.ML ex/TF_Fn.thy ex/twos_compl.ML |
39 ex/TF_Fn.ML ex/TF_Fn.thy ex/twos_compl.ML |
40 |
40 |
41 #Uses cp rather than make_database because Poly/ML allows only 3 levels |
41 #Uses cp rather than make_database because Poly/ML allows only 3 levels |
42 $(BIN)/ZF: $(BIN)/FOL $(FILES) |
42 $(BIN)/ZF: $(BIN)/FOL $(FILES) |
43 case "$(COMP)" in \ |
43 case "$(COMP)" in \ |