author | wenzelm |
Sat, 14 Nov 1998 13:26:11 +0100 | |
changeset 5864 | 30b6a3251813 |
parent 5040 | 78abd4c4802a |
child 6116 | 8ba2f25610f7 |
permissions | -rw-r--r-- |
(* Title: Pure/General/ROOT.ML ID: $Id$ General tools. *) use "table.ML"; use "object.ML"; use "seq.ML"; use "name_space.ML"; use "position.ML"; use "path.ML"; use "file.ML"; use "history.ML"; structure PureGeneral = struct structure Symtab = Symtab; structure Object = Object; structure Seq = Seq; structure NameSpace = NameSpace; structure Position = Position; structure Path = Path; structure File = File; structure History = History; end;