src/HOL/Makefile
changeset 2534 7a876fc091d6
parent 2450 3ad2493fa0e0
child 2889 a86f3b5f3cc7
     1.1 --- a/src/HOL/Makefile	Tue Jan 21 10:58:32 1997 +0100
     1.2 +++ b/src/HOL/Makefile	Tue Jan 21 11:29:28 1997 +0100
     1.3 @@ -183,8 +183,23 @@
     1.4  	else echo 'exit_use_dir"Lambda";quit();' | $(LOGIC); \
     1.5  	fi
     1.6  
     1.7 -##Type inference for MiniML
     1.8 -MINIML_NAMES = I Maybe MiniML Type W
     1.9 +## Type inference without let
    1.10 +
    1.11 +W0_NAMES = I Maybe MiniML Type W
    1.12 +
    1.13 +W0_FILES = W0/ROOT.ML \
    1.14 +	      $(W0_NAMES:%=W0/%.thy) $(W0_NAMES:%=W0/%.ML)
    1.15 +
    1.16 +W0:	$(BIN)/HOL  $(W0_FILES)
    1.17 +	@if [ "$${MAKE_HTML-undefined}" != "undefined" ]; \
    1.18 +	then echo 'make_html := true; exit_use_dir"W0";quit();' \
    1.19 +	       | $(LOGIC);\
    1.20 +	else echo 'exit_use_dir"W0";quit();' | $(LOGIC); \
    1.21 +	fi
    1.22 +
    1.23 +## Type inference with let
    1.24 +
    1.25 +MINIML_NAMES = Generalize Instance Maybe MiniML Type W
    1.26  
    1.27  MINIML_FILES = MiniML/ROOT.ML \
    1.28  	      $(MINIML_NAMES:%=MiniML/%.thy) $(MINIML_NAMES:%=MiniML/%.ML)