src/Pure/Syntax/ROOT.ML
changeset 2198 0dddd9575717
parent 1506 192c48376d25
child 2361 74c99949ad84
equal deleted inserted replaced
2197:e895937fcd56 2198:0dddd9575717
     3     Author:     Tobias Nipkow and Markus Wenzel, TU Muenchen
     3     Author:     Tobias Nipkow and Markus Wenzel, TU Muenchen
     4 
     4 
     5 This file builds the syntax module.
     5 This file builds the syntax module.
     6 *)
     6 *)
     7 
     7 
       
     8 use "symbol_font.ML";
     8 use "pretty.ML";
     9 use "pretty.ML";
     9 use "lexicon.ML";
    10 use "lexicon.ML";
    10 use "ast.ML";
    11 use "ast.ML";
    11 use "syn_ext.ML";
    12 use "syn_ext.ML";
    12 use "parser.ML";
    13 use "parser.ML";