equal
deleted
inserted
replaced
59 |
59 |
60 EX_FILES = ex/ROOT.ML ex/loeckx.ML $(EX_THYS) $(EX_THYS:.thy=.ML) |
60 EX_FILES = ex/ROOT.ML ex/loeckx.ML $(EX_THYS) $(EX_THYS:.thy=.ML) |
61 |
61 |
62 test: ex/ROOT.ML $(BIN)/HOLCF $(EX_FILES) |
62 test: ex/ROOT.ML $(BIN)/HOLCF $(EX_FILES) |
63 case "$(COMP)" in \ |
63 case "$(COMP)" in \ |
64 poly*) echo 'exit_use"ex/ROOT.ML"; quit();' | $(COMP) $(BIN)/HOLCF ;;\ |
64 poly*) echo 'exit_use_dir"ex"; quit();' | $(COMP) $(BIN)/HOLCF ;;\ |
65 sml*) echo 'exit_use"ex/ROOT.ML"' | $(BIN)/HOLCF;;\ |
65 sml*) echo 'exit_use_dir"ex"' | $(BIN)/HOLCF;;\ |
66 *) echo Bad value for ISABELLECOMP: \ |
66 *) echo Bad value for ISABELLECOMP: \ |
67 $(COMP) is not poly or sml;;\ |
67 $(COMP) is not poly or sml;;\ |
68 esac |
68 esac |
69 |
69 |
70 EXPLICIT_DOMAINS_THYS = explicit_domains/Coind.thy explicit_domains/Dlist.thy \ |
70 EXPLICIT_DOMAINS_THYS = explicit_domains/Coind.thy explicit_domains/Dlist.thy \ |
75 EXPLICIT_DOMAINS_FILES = explicit_domains/ROOT.ML $(EXPLICIT_DOMAINS_THYS)\ |
75 EXPLICIT_DOMAINS_FILES = explicit_domains/ROOT.ML $(EXPLICIT_DOMAINS_THYS)\ |
76 $(EXPLICIT_DOMAINS_THYS:.thy=.ML) |
76 $(EXPLICIT_DOMAINS_THYS:.thy=.ML) |
77 |
77 |
78 test2: explicit_domains/ROOT.ML $(BIN)/HOLCF $(EXPLICIT_DOMAINS_FILES) |
78 test2: explicit_domains/ROOT.ML $(BIN)/HOLCF $(EXPLICIT_DOMAINS_FILES) |
79 case "$(COMP)" in \ |
79 case "$(COMP)" in \ |
80 poly*) echo 'exit_use"explicit_domains/ROOT.ML"; quit();' | $(COMP) $(BIN)/HOLCF ;;\ |
80 poly*) echo 'exit_use_dir"explicit_domains"; quit();' \ |
81 sml*) echo 'exit_use"explicit_domains/ROOT.ML"' | $(BIN)/HOLCF;;\ |
81 | $(COMP) $(BIN)/HOLCF ;;\ |
|
82 sml*) echo 'exit_use_dir"explicit_domains"' | $(BIN)/HOLCF;;\ |
82 *) echo Bad value for ISABELLECOMP: \ |
83 *) echo Bad value for ISABELLECOMP: \ |
83 $(COMP) is not poly or sml;;\ |
84 $(COMP) is not poly or sml;;\ |
84 esac |
85 esac |
85 |
86 |
86 .PRECIOUS: $(BIN)/HOL $(BIN)/HOLCF |
87 .PRECIOUS: $(BIN)/HOL $(BIN)/HOLCF |