(* Title: Pure/Syntax/ROOT.ML ID: $Id: ROOT.ML,v 1.24 2005/04/23 17:51:24 wenzelm Exp $ Author: Tobias Nipkow and Markus Wenzel, TU Muenchen This file builds the syntax module. *) use "lexicon.ML"; use "ast.ML"; use "syn_ext.ML"; use "parser.ML"; use "type_ext.ML"; use "syn_trans.ML"; use "mixfix.ML"; use "printer.ML"; use "syntax.ML"; (*hiding private stuff*) structure Lexicon = Hidden; structure Ast = Hidden; structure SynExt = Hidden; structure Parser = Hidden; structure TypeExt = Hidden; structure SynTrans = Hidden; structure Mixfix = Hidden; structure Printer = Hidden;