equal
deleted
inserted
replaced
24 |
24 |
25 CCL_FILES = ccl.thy ccl.ML term.thy term.ML type.thy type.ML \ |
25 CCL_FILES = ccl.thy ccl.ML term.thy term.ML type.thy type.ML \ |
26 coinduction.ML hered.thy hered.ML trancl.thy trancl.ML\ |
26 coinduction.ML hered.thy hered.ML trancl.thy trancl.ML\ |
27 wfd.thy wfd.ML genrec.ML typecheck.ML eval.ML fix.thy fix.ML |
27 wfd.thy wfd.ML genrec.ML typecheck.ML eval.ML fix.thy fix.ML |
28 |
28 |
|
29 EX_FILES = ex/ROOT.ML ex/flag.ML ex/flag.thy ex/list.ML ex/list.thy\ |
|
30 ex/nat.ML ex/nat.thy ex/stream.ML ex/stream.thy |
|
31 |
29 #Uses cp rather than make_database because Poly/ML allows only 3 levels |
32 #Uses cp rather than make_database because Poly/ML allows only 3 levels |
30 $(BIN)/CCL: $(BIN)/FOL $(SET_FILES) $(CCL_FILES) |
33 $(BIN)/CCL: $(BIN)/FOL $(SET_FILES) $(CCL_FILES) |
31 case "$(COMP)" in \ |
34 case "$(COMP)" in \ |
32 poly*) cp $(BIN)/FOL $(BIN)/CCL;\ |
35 poly*) cp $(BIN)/FOL $(BIN)/CCL;\ |
33 echo 'open PolyML; use"ROOT";' | $(COMP) $(BIN)/CCL ;;\ |
36 echo 'open PolyML; use"ROOT";' | $(COMP) $(BIN)/CCL ;;\ |
36 esac |
39 esac |
37 |
40 |
38 $(BIN)/FOL: |
41 $(BIN)/FOL: |
39 cd ../FOL; $(MAKE) |
42 cd ../FOL; $(MAKE) |
40 |
43 |
41 test: ex/ROOT.ML $(BIN)/CCL |
44 test: ex/ROOT.ML $(BIN)/CCL $(EX_FILES) |
42 case "$(COMP)" in \ |
45 case "$(COMP)" in \ |
43 poly*) echo 'use"ex/ROOT.ML"; quit();' | $(COMP) $(BIN)/CCL ;;\ |
46 poly*) echo 'use"ex/ROOT.ML"; quit();' | $(COMP) $(BIN)/CCL ;;\ |
44 sml*) echo 'use"ex/ROOT.ML";' | $(BIN)/CCL;;\ |
47 sml*) echo 'use"ex/ROOT.ML";' | $(BIN)/CCL;;\ |
45 *) echo Bad value for ISABELLECOMP;;\ |
48 *) echo Bad value for ISABELLECOMP;;\ |
46 esac |
49 esac |