src/HOLCF/Makefile
changeset 2679 3eac428cdd1b
parent 2640 ee4dfce170a0
child 3028 45204c79ad1d
     1.1 --- a/src/HOLCF/Makefile	Mon Feb 24 09:46:12 1997 +0100
     1.2 +++ b/src/HOLCF/Makefile	Mon Feb 24 16:12:24 1997 +0100
     1.3 @@ -86,29 +86,5 @@
     1.4  			\"$(COMP)\" is not poly or sml;;\
     1.5  	esac
     1.6  
     1.7 -#EXPLICIT_DOMAINS_THYS = explicit_domains/Dnat.thy explicit_domains/Dnat2.thy \
     1.8 -#		explicit_domains/Dlist.thy \
     1.9 -#		explicit_domains/Stream.thy explicit_domains/Stream2.thy
    1.10 -
    1.11 -#EXPLICIT_DOMAINS_FILES = explicit_domains/ROOT.ML $(EXPLICIT_DOMAINS_THYS)\
    1.12 -#			 $(EXPLICIT_DOMAINS_THYS:.thy=.ML)
    1.13 -
    1.14 -#test2:	explicit_domains/ROOT.ML  $(BIN)/HOLCF	$(EXPLICIT_DOMAINS_FILES) 
    1.15 -#	@case `basename "$(COMP)"` in \
    1.16 -#	poly*)	if [ "$${MAKE_HTML-undefined}" != "undefined" ]; \
    1.17 -#		then echo 'make_html := true; exit_use_dir"explicit_domains";\
    1.18 -#			  quit();' | $(COMP) $(BIN)/HOLCF;\
    1.19 -#		else echo 'exit_use_dir"explicit_domains"; quit();' \
    1.20 -#		       | $(COMP) $(BIN)/HOLCF;\
    1.21 -#		fi;;\
    1.22 -#	sml*)	if [ "$${MAKE_HTML-undefined}" != "undefined" ]; \
    1.23 -#		then echo 'make_html := true; exit_use_dir"exlicit_domains";' \
    1.24 -#		       | $(BIN)/HOLCF;\
    1.25 -#		else echo 'exit_use_dir"explicit_domains";' | $(BIN)/HOLCF;\
    1.26 -#		fi;;\
    1.27 -#	*)	echo Bad value for ISABELLECOMP: \
    1.28 -#			\"$(COMP)\" is not poly or sml;;\
    1.29 -#	esac
    1.30 -
    1.31  .PRECIOUS:  $(BIN)/HOL	$(BIN)/HOLCF 
    1.32