equal
deleted
inserted
replaced
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 axclass.ML install_pp.ML |
25 drule.ML tctical.ML tactic.ML goals.ML axclass.ML install_pp.ML |
26 |
26 |
27 SYNTAX_FILES = Syntax/ROOT.ML Syntax/ast.ML Syntax/lexicon.ML\ |
27 SYNTAX_FILES = Syntax/ROOT.ML Syntax/ast.ML Syntax/lexicon.ML\ |
28 Syntax/parser.ML Syntax/type_ext.ML Syntax/sextension.ML\ |
28 Syntax/parser.ML Syntax/type_ext.ML Syntax/syn_trans.ML\ |
29 Syntax/pretty.ML Syntax/printer.ML Syntax/syntax.ML\ |
29 Syntax/pretty.ML Syntax/printer.ML Syntax/syntax.ML\ |
30 Syntax/syn_ext.ML Syntax/mixfix.ML |
30 Syntax/syn_ext.ML Syntax/mixfix.ML |
31 |
31 |
32 THY_FILES = Thy/ROOT.ML Thy/thy_scan.ML Thy/thy_parse.ML\ |
32 THY_FILES = Thy/ROOT.ML Thy/thy_scan.ML Thy/thy_parse.ML\ |
33 Thy/thy_syn.ML Thy/thy_read.ML |
33 Thy/thy_syn.ML Thy/thy_read.ML |