| author | paulson |
| Fri, 08 Nov 2002 10:34:40 +0100 | |
| changeset 13702 | c7cf8fa66534 |
| parent 12785 | 27debaf2112d |
| child 14981 | e73f8140af78 |
| permissions | -rw-r--r-- |
| 18 | 1 |
(* Title: Pure/Syntax/ROOT.ML |
| 0 | 2 |
ID: $Id$ |
3 |
Author: Tobias Nipkow and Markus Wenzel, TU Muenchen |
|
| 12785 | 4 |
License: GPL (GNU GENERAL PUBLIC LICENSE) |
| 0 | 5 |
|
| 18 | 6 |
This file builds the syntax module. |
| 0 | 7 |
*) |
8 |
||
| 239 | 9 |
use "lexicon.ML"; |
| 2691 | 10 |
use "token_trans.ML"; |
| 0 | 11 |
use "ast.ML"; |
| 239 | 12 |
use "syn_ext.ML"; |
| 18 | 13 |
use "parser.ML"; |
| 0 | 14 |
use "type_ext.ML"; |
|
549
5d904be18774
replaced SExtension by SynTrans (mixfix stuff in Mixfix);
wenzelm
parents:
417
diff
changeset
|
15 |
use "syn_trans.ML"; |
| 392 | 16 |
use "mixfix.ML"; |
| 0 | 17 |
use "printer.ML"; |
18 |
use "syntax.ML"; |
|
19 |
||
| 5683 | 20 |
(*hiding private stuff*) |
21 |
structure Lexicon = Hidden; |
|
22 |
structure TokenTrans = Hidden; |
|
23 |
structure Ast = Hidden; |
|
24 |
structure SynExt = Hidden; |
|
25 |
structure Parser = Hidden; |
|
26 |
structure TypeExt = Hidden; |
|
27 |
structure SynTrans = Hidden; |
|
28 |
structure Mixfix = Hidden; |
|
29 |
structure Printer = Hidden; |