changeset 4940 | dd4bbbcd1d22 |
parent 4696 | ff89fc67cc7a |
child 5230 | fdc28193ccf7 |
--- a/src/Pure/Syntax/ROOT.ML Mon May 18 18:08:58 1998 +0200 +++ b/src/Pure/Syntax/ROOT.ML Mon May 18 18:10:04 1998 +0200 @@ -5,9 +5,13 @@ This file builds the syntax module. *) +(*generic modules*) use "pretty.ML"; use "scan.ML"; +use "source.ML"; use "symbol.ML"; + +(*actual syntax module*) use "lexicon.ML"; use "token_trans.ML"; use "ast.ML";