changeset 2198 | 0dddd9575717 |
parent 1506 | 192c48376d25 |
child 2361 | 74c99949ad84 |
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"; |