src/HOL/Makefile
changeset 1125 13a3df2adbe5
parent 1063 d33e3523a5e6
child 1129 866fff857626
     1.1 --- a/src/HOL/Makefile	Mon May 22 14:12:40 1995 +0200
     1.2 +++ b/src/HOL/Makefile	Mon May 22 15:58:57 1995 +0200
     1.3 @@ -98,6 +98,15 @@
     1.4  Subst:  $(BIN)/CHOL  $(SUBST_FILES)
     1.5  	echo 'exit_use"Subst/ROOT.ML";quit();' | $(LOGIC)
     1.6  
     1.7 +##Confluence of Lambda-calculus
     1.8 +LAMBDA_NAMES = Lambda ParRed Confluence
     1.9 +
    1.10 +LAMBDA_FILES = Lambda/ROOT.ML \
    1.11 +              $(LAMBDA_NAMES:%=Lambda/%.thy) $(LAMBDA_NAMES:%=Lambda/%.ML)
    1.12 +
    1.13 +Lambda:  $(BIN)/CHOL  $(LAMBDA_FILES)
    1.14 +	echo 'exit_use"Lambda/ROOT.ML";quit();' | $(LOGIC)
    1.15 +
    1.16  ##Miscellaneous examples
    1.17  EX_NAMES = LexProd MT Acc PropLog Puzzle Qsort LList Rec Simult Term String 
    1.18  
    1.19 @@ -108,7 +117,7 @@
    1.20  	echo 'exit_use"ex/ROOT.ML";quit();' | $(LOGIC)
    1.21  
    1.22  #Full test.
    1.23 -test:   $(BIN)/CHOL IMP Integ IOA Subst ex
    1.24 +test:   $(BIN)/CHOL IMP Integ IOA Subst Lambda ex
    1.25  	echo 'Test examples ran successfully' > test
    1.26  
    1.27  .PRECIOUS:  $(BIN)/Pure $(BIN)/CHOL