src/Pure/Syntax/ROOT.ML
author paulson
Thu Sep 25 12:09:41 1997 +0200 (1997-09-25)
changeset 3706 e57b5902822f
parent 2691 d696d7e17046
child 4696 ff89fc67cc7a
permissions -rw-r--r--
Generalized and exported biresolution_from_nets_tac to allow the declaration
of Clarify_tac
     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 "pretty.ML";
     9 use "lexicon.ML";
    10 structure Scanner: SCANNER = Lexicon;
    11 use "symbol_font.ML";
    12 use "token_trans.ML";
    13 use "ast.ML";
    14 use "syn_ext.ML";
    15 use "parser.ML";
    16 use "type_ext.ML";
    17 use "syn_trans.ML";
    18 use "mixfix.ML";
    19 use "printer.ML";
    20 use "syntax.ML";
    21 
    22 (*hiding: only the most basic features are opened*)
    23 structure BasicSyntax: BASIC_SYNTAX = Syntax;
    24 open BasicSyntax;