equal
deleted
inserted
replaced
30 ex/Modal/ROOT.ML ex/Modal/S43thms.ML ex/Modal/S4thms.ML ex/Modal/Tthms.ML \ |
30 ex/Modal/ROOT.ML ex/Modal/S43thms.ML ex/Modal/S4thms.ML ex/Modal/Tthms.ML \ |
31 ex/ILL/ILL_kleene_lemmas.ML \ |
31 ex/ILL/ILL_kleene_lemmas.ML \ |
32 $(ILL_NAMES:%=ex/ILL/%.thy) $(ILL_NAMES:%=ex/ILL/%.ML) |
32 $(ILL_NAMES:%=ex/ILL/%.thy) $(ILL_NAMES:%=ex/ILL/%.ML) |
33 |
33 |
34 $(BIN)/Sequents: $(BIN)/Pure $(FILES) |
34 $(BIN)/Sequents: $(BIN)/Pure $(FILES) |
35 @case `expr "//$(COMP)" : '[^ ]*/\(.*\)'` in \ |
35 @case `basename "$(COMP)"` in \ |
36 poly*) echo 'make_database"$(BIN)/Sequents"; quit();' \ |
36 poly*) echo 'make_database"$(BIN)/Sequents"; quit();' \ |
37 | $(COMP) $(BIN)/Pure;\ |
37 | $(COMP) $(BIN)/Pure;\ |
38 if [ "$${MAKE_HTML}" = "true" ]; \ |
38 if [ "$${MAKE_HTML}" = "true" ]; \ |
39 then echo 'open PolyML; make_html := true; exit_use_dir".";' \ |
39 then echo 'open PolyML; make_html := true; exit_use_dir".";' \ |
40 | $(COMP) $(BIN)/Sequents;\ |
40 | $(COMP) $(BIN)/Sequents;\ |
57 |
57 |
58 $(BIN)/Pure: |
58 $(BIN)/Pure: |
59 cd ../Pure; $(MAKE) |
59 cd ../Pure; $(MAKE) |
60 |
60 |
61 test: $(BIN)/Sequents $(EX_FILES) |
61 test: $(BIN)/Sequents $(EX_FILES) |
62 @case `expr "//$(COMP)" : '[^ ]*/\(.*\)'` in \ |
62 @case `basename "$(COMP)"` in \ |
63 poly*) echo 'exit_use"ex/ROOT.ML";quit();' | $(COMP) $(BIN)/Sequents;;\ |
63 poly*) echo 'exit_use"ex/ROOT.ML";quit();' | $(COMP) $(BIN)/Sequents;;\ |
64 sml*) echo 'exit_use"ex/ROOT.ML";' | $(BIN)/Sequents;;\ |
64 sml*) echo 'exit_use"ex/ROOT.ML";' | $(BIN)/Sequents;;\ |
65 *) echo Bad value for ISABELLECOMP: \ |
65 *) echo Bad value for ISABELLECOMP: \ |
66 \"$(COMP)\" is not poly or sml;;\ |
66 \"$(COMP)\" is not poly or sml;;\ |
67 esac |
67 esac |