equal
deleted
inserted
replaced
14 #Makes HOL Isabelle if this file is ABSENT -- but not |
14 #Makes HOL Isabelle if this file is ABSENT -- but not |
15 #if it is out of date, since this Makefile does not know its dependencies! |
15 #if it is out of date, since this Makefile does not know its dependencies! |
16 |
16 |
17 BIN = $(ISABELLEBIN) |
17 BIN = $(ISABELLEBIN) |
18 COMP = $(ISABELLECOMP) |
18 COMP = $(ISABELLECOMP) |
19 FILES = ROOT.ML void.thy void.ML porder.thy porder.ML pcpo.thy \ |
19 FILES = ROOT.ML Void.thy Void.ML Porder.thy Porder.ML Pcpo.thy \ |
20 pcpo.ML fun1.thy fun1.ML fun2.thy fun2.ML fun3.thy fun3.ML \ |
20 Pcpo.ML Fun1.thy Fun1.ML Fun2.thy Fun2.ML Fun3.thy Fun3.ML \ |
21 cfun1.thy cfun1.ML cfun2.thy cfun2.ML cfun3.thy cfun3.ML \ |
21 Cfun1.thy Cfun1.ML Cfun2.thy Cfun2.ML Cfun3.thy Cfun3.ML \ |
22 cinfix.ML\ |
22 cinfix.ML\ |
23 sprod0.thy sprod0.ML sprod1.thy sprod1.ML sprod2.thy sprod2.ML\ |
23 Sprod0.thy Sprod0.ML Sprod1.thy Sprod1.ML Sprod2.thy Sprod2.ML\ |
24 sprod3.thy sprod3.ML |
24 Sprod3.thy Sprod3.ML |
25 |
25 |
26 EX_FILES = ex/coind.thy ex/coind.ML \ |
26 EX_FILES = ex/Coind.thy ex/Coind.ML \ |
27 ex/hoare.thy ex/hoare.ML ex/loop.thy ex/loop.ML |
27 ex/Hoare.thy ex/Hoare.ML ex/Loop.thy ex/Loop.ML |
28 |
28 |
29 $(BIN)/HOLCF: $(BIN)/HOL $(FILES) |
29 $(BIN)/HOLCF: $(BIN)/HOL $(FILES) |
30 case "$(COMP)" in \ |
30 case "$(COMP)" in \ |
31 poly*) echo 'make_database"$(BIN)/HOLCF"; quit();' \ |
31 poly*) echo 'make_database"$(BIN)/HOLCF"; quit();' \ |
32 | $(COMP) $(BIN)/HOL ;\ |
32 | $(COMP) $(BIN)/HOL ;\ |