equal
deleted
inserted
replaced
7 # are loaded on top of it. |
7 # are loaded on top of it. |
8 # |
8 # |
9 |
9 |
10 OUT = $(ISABELLE_OUTPUT) |
10 OUT = $(ISABELLE_OUTPUT) |
11 |
11 |
12 FILES = ML-Systems/polyml.ML ML-Systems/smlnj-0.93.ML \ |
12 FILES = ML-Systems/mlworks.ML ML-Systems/polyml.ML ML-Systems/smlnj-0.93.ML \ |
13 ML-Systems/smlnj.ML ROOT.ML Syntax/ROOT.ML Syntax/ast.ML \ |
13 ML-Systems/smlnj.ML ROOT.ML Syntax/ROOT.ML Syntax/ast.ML \ |
14 Syntax/lexicon.ML Syntax/mixfix.ML Syntax/parser.ML Syntax/pretty.ML \ |
14 Syntax/lexicon.ML Syntax/mixfix.ML Syntax/parser.ML Syntax/pretty.ML \ |
15 Syntax/printer.ML Syntax/symbol_font.ML Syntax/syn_ext.ML \ |
15 Syntax/printer.ML Syntax/symbol_font.ML Syntax/syn_ext.ML \ |
16 Syntax/syn_trans.ML Syntax/syntax.ML Syntax/token_trans.ML \ |
16 Syntax/syn_trans.ML Syntax/syntax.ML Syntax/token_trans.ML \ |
17 Syntax/type_ext.ML Thy/ROOT.ML Thy/browser_info.ML Thy/context.ML Thy/file.ML \ |
17 Syntax/type_ext.ML Thy/ROOT.ML Thy/browser_info.ML Thy/context.ML Thy/file.ML \ |