src/Pure/Makefile
changeset 57 87e14d7f20dc
parent 0 a5a9c433f639
child 223 7892b76adb5b
equal deleted inserted replaced
56:2caa6f49f06e 57:87e14d7f20dc
    20 
    20 
    21 BIN = $(ISABELLEBIN)
    21 BIN = $(ISABELLEBIN)
    22 COMP = $(ISABELLECOMP)
    22 COMP = $(ISABELLECOMP)
    23 FILES =	POLY.ML NJ.ML ROOT.ML library.ML term.ML symtab.ML type.ML sign.ML\
    23 FILES =	POLY.ML NJ.ML ROOT.ML library.ML term.ML symtab.ML type.ML sign.ML\
    24 	sequence.ML envir.ML pattern.ML unify.ML logic.ML thm.ML net.ML\
    24 	sequence.ML envir.ML pattern.ML unify.ML logic.ML thm.ML net.ML\
    25 	drule.ML tctical.ML tactic.ML goals.ML
    25 	drule.ML tctical.ML tactic.ML goals.ML install_pp.ML
    26 
    26 
    27 SYNTAX_FILES =  Syntax/ROOT.ML	Syntax/ast.ML		Syntax/xgram.ML\
    27 SYNTAX_FILES =  Syntax/ROOT.ML	Syntax/ast.ML		Syntax/xgram.ML\
    28 	Syntax/extension.ML	Syntax/lexicon.ML	Syntax/parse_tree.ML\
    28 	Syntax/extension.ML	Syntax/lexicon.ML	Syntax/parse_tree.ML\
    29 	Syntax/earley0A.ML	Syntax/type_ext.ML	Syntax/sextension.ML\
    29 	Syntax/parser.ML	Syntax/type_ext.ML	Syntax/sextension.ML\
    30 	Syntax/pretty.ML	Syntax/printer.ML	Syntax/syntax.ML
    30 	Syntax/pretty.ML	Syntax/printer.ML	Syntax/syntax.ML\
       
    31 	Syntax/earley0A.ML
    31 
    32 
    32 THY_FILES = Thy/ROOT.ML Thy/scan.ML Thy/parse.ML Thy/syntax.ML Thy/read.ML
    33 THY_FILES = Thy/ROOT.ML Thy/scan.ML Thy/parse.ML Thy/syntax.ML Thy/read.ML
    33 
    34 
    34 #Uses cp rather than make_database because Poly/ML allows only 3 levels
    35 #Uses cp rather than make_database because Poly/ML allows only 3 levels
    35 $(BIN)/Pure:   $(FILES)  $(SYNTAX_FILES)  $(THY_FILES)  $(ML_DBASE)
    36 $(BIN)/Pure:   $(FILES)  $(SYNTAX_FILES)  $(THY_FILES)  $(ML_DBASE)