src/Pure/Syntax/ROOT.ML
author wenzelm
Wed Oct 31 21:59:07 2001 +0100 (2001-10-31)
changeset 12004 1703de633aaf
parent 6116 8ba2f25610f7
child 12785 27debaf2112d
permissions -rw-r--r--
IsarThy.theorem_i: no locale;
wenzelm@18
     1
(*  Title:      Pure/Syntax/ROOT.ML
clasohm@0
     2
    ID:         $Id$
clasohm@0
     3
    Author:     Tobias Nipkow and Markus Wenzel, TU Muenchen
clasohm@0
     4
wenzelm@18
     5
This file builds the syntax module.
clasohm@0
     6
*)
clasohm@0
     7
wenzelm@239
     8
use "lexicon.ML";
wenzelm@2691
     9
use "token_trans.ML";
clasohm@0
    10
use "ast.ML";
wenzelm@239
    11
use "syn_ext.ML";
wenzelm@18
    12
use "parser.ML";
clasohm@0
    13
use "type_ext.ML";
wenzelm@549
    14
use "syn_trans.ML";
wenzelm@392
    15
use "mixfix.ML";
clasohm@0
    16
use "printer.ML";
clasohm@0
    17
use "syntax.ML";
clasohm@0
    18
wenzelm@5683
    19
(*hiding private stuff*)
wenzelm@5683
    20
structure Lexicon = Hidden;
wenzelm@5683
    21
structure TokenTrans = Hidden;
wenzelm@5683
    22
structure Ast = Hidden;
wenzelm@5683
    23
structure SynExt = Hidden;
wenzelm@5683
    24
structure Parser = Hidden;
wenzelm@5683
    25
structure TypeExt = Hidden;
wenzelm@5683
    26
structure SynTrans = Hidden;
wenzelm@5683
    27
structure Mixfix = Hidden;
wenzelm@5683
    28
structure Printer = Hidden;