19 #Makes HOL Isabelle if this file is ABSENT -- but not |
19 #Makes HOL Isabelle if this file is ABSENT -- but not |
20 #if it is out of date, since this Makefile does not know its dependencies! |
20 #if it is out of date, since this Makefile does not know its dependencies! |
21 |
21 |
22 BIN = $(ISABELLEBIN) |
22 BIN = $(ISABELLEBIN) |
23 COMP = $(ISABELLECOMP) |
23 COMP = $(ISABELLECOMP) |
24 THYS = Holcfb.thy Void.thy Porder.thy Pcpo.thy \ |
24 THYS = Void.thy Porder.thy Pcpo.thy \ |
25 Fun1.thy Fun2.thy Fun3.thy \ |
25 Fun1.thy Fun2.thy Fun3.thy \ |
26 Cfun1.thy Cfun2.thy Cfun3.thy Cont.thy \ |
26 Cfun1.thy Cfun2.thy Cfun3.thy Cont.thy \ |
27 Cprod1.thy Cprod2.thy Cprod3.thy \ |
27 Cprod1.thy Cprod2.thy Cprod3.thy \ |
28 Sprod0.thy Sprod1.thy Sprod2.thy Sprod3.thy \ |
28 Sprod0.thy Sprod1.thy Sprod2.thy Sprod3.thy \ |
29 Ssum0.thy Ssum1.thy Ssum2.thy Ssum3.thy \ |
29 Ssum0.thy Ssum1.thy Ssum2.thy Ssum3.thy \ |
30 Up1.thy Up2.thy Up3.thy Fix.thy ccc1.thy One.thy \ |
30 Up1.thy Up2.thy Up3.thy Fix.thy ccc1.thy One.thy \ |
31 Tr1.thy Tr2.thy HOLCF.thy |
31 Tr1.thy Tr2.thy Lift1.thy Lift2.thy Lift2.thy HOLCF.thy |
32 |
32 |
33 FILES = ROOT.ML Porder0.thy $(THYS) $(THYS:.thy=.ML) |
33 FILES = ROOT.ML Porder0.thy $(THYS) $(THYS:.thy=.ML) |
34 |
34 |
35 #Uses cp rather than make_database because Poly/ML allows only 3 levels |
35 #Uses cp rather than make_database because Poly/ML allows only 3 levels |
36 $(BIN)/HOLCF: $(BIN)/HOL $(FILES) |
36 $(BIN)/HOLCF: $(BIN)/HOL $(FILES) |