src/HOL/Makefile
changeset 1699 0bcc8cab3461
parent 1698 bf46e4acc682
child 1797 334308d2afbc
equal deleted inserted replaced
1698:bf46e4acc682 1699:0bcc8cab3461
    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 Natural Transition Denotation Hoare VC
    77 IMP_NAMES = Expr 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); \