src/HOL/Makefile
changeset 1301 42782316d510
parent 1296 ae31bb7774a7
child 1329 8987c0df4b2f
     1.1 --- a/src/HOL/Makefile	Wed Oct 25 09:46:46 1995 +0100
     1.2 +++ b/src/HOL/Makefile	Wed Oct 25 09:48:29 1995 +0100
     1.3 @@ -119,6 +119,14 @@
     1.4  Lambda:  $(BIN)/HOL  $(LAMBDA_FILES)
     1.5  	echo 'exit_use"Lambda/ROOT.ML";quit();' | $(LOGIC)
     1.6  
     1.7 +MINIML_NAMES = I Maybe MiniML Type W
     1.8 +
     1.9 +LAMBDA_FILES = MiniML/ROOT.ML \
    1.10 +              $(MINIML_NAMES:%=MiniML/%.thy) $(MINIML_NAMES:%=MiniML/%.ML)
    1.11 +
    1.12 +MiniML: $(BIN)/HOL  $(MINIML_FILES)
    1.13 +	echo 'exit_use"MiniML/ROOT.ML";quit();' | $(LOGIC)
    1.14 +
    1.15  ##Miscellaneous examples
    1.16  EX_NAMES = LexProd MT Acc PropLog Puzzle Qsort LList Rec Simult Term String \
    1.17  	   BT Perm
    1.18 @@ -130,7 +138,7 @@
    1.19  	echo 'exit_use"ex/ROOT.ML";quit();' | $(LOGIC)
    1.20  
    1.21  #Full test. (IOA has been removed temporarily)
    1.22 -test:   $(BIN)/HOL IMP Integ Subst Lambda ex
    1.23 +test:   $(BIN)/HOL IMP Integ Subst Lambda MiniML ex
    1.24  	echo 'Test examples ran successfully' > test
    1.25  
    1.26  .PRECIOUS:  $(BIN)/Pure $(BIN)/HOL