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
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@18
     8
use "pretty.ML";
wenzelm@239
     9
use "lexicon.ML";
wenzelm@2361
    10
structure Scanner: SCANNER = Lexicon;
wenzelm@2361
    11
use "symbol_font.ML";
wenzelm@2691
    12
use "token_trans.ML";
clasohm@0
    13
use "ast.ML";
wenzelm@239
    14
use "syn_ext.ML";
wenzelm@18
    15
use "parser.ML";
clasohm@0
    16
use "type_ext.ML";
wenzelm@549
    17
use "syn_trans.ML";
wenzelm@392
    18
use "mixfix.ML";
clasohm@0
    19
use "printer.ML";
clasohm@0
    20
use "syntax.ML";
clasohm@0
    21
wenzelm@2361
    22
(*hiding: only the most basic features are opened*)
paulson@1506
    23
structure BasicSyntax: BASIC_SYNTAX = Syntax;
paulson@1506
    24
open BasicSyntax;