equal
deleted
inserted
replaced
72 *) echo "echo Bad value for ISABELLECOMP: \ |
72 *) echo "echo Bad value for ISABELLECOMP: \ |
73 $ISABELLEBIN is not poly or sml; exit 1" ;;\ |
73 $ISABELLEBIN is not poly or sml; exit 1" ;;\ |
74 esac |
74 esac |
75 |
75 |
76 ##IMP-semantics example |
76 ##IMP-semantics example |
77 IMP_NAMES = Com Denotation Equiv Properties |
77 IMP_NAMES = Com Natural Transition Denotation Hoare VC |
78 IMP_FILES = IMP/ROOT.ML $(IMP_NAMES:%=IMP/%.thy) $(IMP_NAMES:%=IMP/%.ML) |
78 IMP_FILES = IMP/ROOT.ML $(IMP_NAMES:%=IMP/%.thy) $(IMP_NAMES:%=IMP/%.ML) |
79 |
79 |
80 IMP: $(BIN)/HOL $(IMP_FILES) |
80 IMP: $(BIN)/HOL $(IMP_FILES) |
81 if [ "$${MAKE_HTML-undefined}" != "undefined" ]; \ |
81 if [ "$${MAKE_HTML-undefined}" != "undefined" ]; \ |
82 then echo 'make_html := true; exit_use_dir"IMP";quit();' | $(LOGIC); \ |
82 then echo 'make_html := true; exit_use_dir"IMP";quit();' | $(LOGIC); \ |