Added Lex
authornipkow
Fri Nov 17 19:41:20 1995 +0100 (1995-11-17)
changeset 13438770c062b092
parent 1342 f6651b6b0482
child 1344 f172a7f14e49
Added Lex
src/HOL/Makefile
     1.1 --- a/src/HOL/Makefile	Fri Nov 17 15:10:36 1995 +0100
     1.2 +++ b/src/HOL/Makefile	Fri Nov 17 19:41:20 1995 +0100
     1.3 @@ -123,17 +123,27 @@
     1.4  LAMBDA_FILES = Lambda/ROOT.ML \
     1.5                $(LAMBDA_NAMES:%=Lambda/%.thy) $(LAMBDA_NAMES:%=Lambda/%.ML)
     1.6  
     1.7 -Lambda:  $(BIN)/HOL  $(LAMBDA_FILES)
     1.8 +Lambda:	$(BIN)/HOL  $(LAMBDA_FILES)
     1.9  	echo 'exit_use"Lambda/ROOT.ML";quit();' | $(LOGIC)
    1.10  
    1.11 +##Type inference for MiniML
    1.12  MINIML_NAMES = I Maybe MiniML Type W
    1.13  
    1.14 -LAMBDA_FILES = MiniML/ROOT.ML \
    1.15 +MINIML_FILES = MiniML/ROOT.ML \
    1.16                $(MINIML_NAMES:%=MiniML/%.thy) $(MINIML_NAMES:%=MiniML/%.ML)
    1.17  
    1.18 -MiniML: $(BIN)/HOL  $(MINIML_FILES)
    1.19 +MiniML:	$(BIN)/HOL  $(MINIML_FILES)
    1.20  	echo 'exit_use"MiniML/ROOT.ML";quit();' | $(LOGIC)
    1.21  
    1.22 +##Lexical analysis
    1.23 +LEX_FILES = Auto AutoChopper Chopper Prefix
    1.24 +
    1.25 +LEX_FILES = Lex/ROOT.ML \
    1.26 +            $(LEX_NAMES:%=Lex/%.thy) $(LEX_NAMES:%=Lex/%.ML)
    1.27 +
    1.28 +Lex:	$(BIN)/HOL  $(LEX_FILES)
    1.29 +	echo 'exit_use"Lex/ROOT.ML";quit();' | $(LOGIC)
    1.30 +
    1.31  ##Miscellaneous examples
    1.32  EX_NAMES = LexProd MT Acc PropLog Puzzle Qsort LList Rec Simult Term String \
    1.33  	   BT Perm
    1.34 @@ -144,8 +154,8 @@
    1.35  ex:     $(BIN)/HOL  $(EX_FILES)
    1.36  	echo 'exit_use"ex/ROOT.ML";quit();' | $(LOGIC)
    1.37  
    1.38 -#Full test. (IOA has been removed temporarily)
    1.39 -test:   $(BIN)/HOL IMP Hoare Integ Subst Lambda MiniML IOA ex
    1.40 +#Full test.
    1.41 +test:   $(BIN)/HOL IMP Hoare Lex Integ Subst Lambda MiniML IOA ex
    1.42  	echo 'Test examples ran successfully' > test
    1.43  
    1.44  .PRECIOUS:  $(BIN)/Pure $(BIN)/HOL