src/Pure/General/ROOT.ML
author wenzelm
Sat, 14 Nov 1998 13:26:11 +0100
changeset 5864 30b6a3251813
parent 5040 78abd4c4802a
child 6116 8ba2f25610f7
permissions -rw-r--r--
prefixed op;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
5018
ce8e87fad843 General tools.
wenzelm
parents:
diff changeset
     1
(*  Title:      Pure/General/ROOT.ML
ce8e87fad843 General tools.
wenzelm
parents:
diff changeset
     2
    ID:         $Id$
ce8e87fad843 General tools.
wenzelm
parents:
diff changeset
     3
ce8e87fad843 General tools.
wenzelm
parents:
diff changeset
     4
General tools.
ce8e87fad843 General tools.
wenzelm
parents:
diff changeset
     5
*)
ce8e87fad843 General tools.
wenzelm
parents:
diff changeset
     6
ce8e87fad843 General tools.
wenzelm
parents:
diff changeset
     7
use "table.ML";
ce8e87fad843 General tools.
wenzelm
parents:
diff changeset
     8
use "object.ML";
ce8e87fad843 General tools.
wenzelm
parents:
diff changeset
     9
use "seq.ML";
ce8e87fad843 General tools.
wenzelm
parents:
diff changeset
    10
use "name_space.ML";
ce8e87fad843 General tools.
wenzelm
parents:
diff changeset
    11
use "position.ML";
ce8e87fad843 General tools.
wenzelm
parents:
diff changeset
    12
use "path.ML";
ce8e87fad843 General tools.
wenzelm
parents:
diff changeset
    13
use "file.ML";
5040
78abd4c4802a added General/history.ML;
wenzelm
parents: 5018
diff changeset
    14
use "history.ML";
5864
30b6a3251813 prefixed op;
wenzelm
parents: 5040
diff changeset
    15
30b6a3251813 prefixed op;
wenzelm
parents: 5040
diff changeset
    16
structure PureGeneral =
30b6a3251813 prefixed op;
wenzelm
parents: 5040
diff changeset
    17
struct
30b6a3251813 prefixed op;
wenzelm
parents: 5040
diff changeset
    18
  structure Symtab = Symtab;
30b6a3251813 prefixed op;
wenzelm
parents: 5040
diff changeset
    19
  structure Object = Object;
30b6a3251813 prefixed op;
wenzelm
parents: 5040
diff changeset
    20
  structure Seq = Seq;
30b6a3251813 prefixed op;
wenzelm
parents: 5040
diff changeset
    21
  structure NameSpace = NameSpace;
30b6a3251813 prefixed op;
wenzelm
parents: 5040
diff changeset
    22
  structure Position = Position;
30b6a3251813 prefixed op;
wenzelm
parents: 5040
diff changeset
    23
  structure Path = Path;
30b6a3251813 prefixed op;
wenzelm
parents: 5040
diff changeset
    24
  structure File = File;
30b6a3251813 prefixed op;
wenzelm
parents: 5040
diff changeset
    25
  structure History = History;
30b6a3251813 prefixed op;
wenzelm
parents: 5040
diff changeset
    26
end;