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;
     1 (*  Title:      Pure/Syntax/ROOT.ML
     2     ID:         $Id$
     3     Author:     Tobias Nipkow and Markus Wenzel, TU Muenchen
     4 
     5 This file builds the syntax module.
     6 *)
     7 
     8 use "lexicon.ML";
     9 use "token_trans.ML";
    10 use "ast.ML";
    11 use "syn_ext.ML";
    12 use "parser.ML";
    13 use "type_ext.ML";
    14 use "syn_trans.ML";
    15 use "mixfix.ML";
    16 use "printer.ML";
    17 use "syntax.ML";
    18 
    19 (*hiding private stuff*)
    20 structure Lexicon = Hidden;
    21 structure TokenTrans = Hidden;
    22 structure Ast = Hidden;
    23 structure SynExt = Hidden;
    24 structure Parser = Hidden;
    25 structure TypeExt = Hidden;
    26 structure SynTrans = Hidden;
    27 structure Mixfix = Hidden;
    28 structure Printer = Hidden;