equal
deleted
inserted
replaced
28 NJ093.ML NJ1xx.ML ../Provers/simplifier.ML |
28 NJ093.ML NJ1xx.ML ../Provers/simplifier.ML |
29 |
29 |
30 SYNTAX_FILES = Syntax/ROOT.ML Syntax/ast.ML Syntax/lexicon.ML\ |
30 SYNTAX_FILES = Syntax/ROOT.ML Syntax/ast.ML Syntax/lexicon.ML\ |
31 Syntax/parser.ML Syntax/type_ext.ML Syntax/syn_trans.ML\ |
31 Syntax/parser.ML Syntax/type_ext.ML Syntax/syn_trans.ML\ |
32 Syntax/pretty.ML Syntax/printer.ML Syntax/syntax.ML\ |
32 Syntax/pretty.ML Syntax/printer.ML Syntax/syntax.ML\ |
33 Syntax/syn_ext.ML Syntax/mixfix.ML |
33 Syntax/syn_ext.ML Syntax/mixfix.ML Syntax/symbol_font.ML |
34 |
34 |
35 THY_FILES = Thy/ROOT.ML Thy/thy_scan.ML Thy/thy_parse.ML\ |
35 THY_FILES = Thy/ROOT.ML Thy/thy_scan.ML Thy/thy_parse.ML\ |
36 Thy/thy_syn.ML Thy/thy_read.ML Thy/thm_database.ML |
36 Thy/thy_syn.ML Thy/thy_read.ML Thy/thm_database.ML |
37 |
37 |
38 #Uses cp rather than make_database because Poly/ML allows only 3 levels |
38 #Uses cp rather than make_database because Poly/ML allows only 3 levels |