src/Pure/General/ROOT.ML
author wenzelm
Thu, 04 Feb 1999 18:12:26 +0100
changeset 6222 2b24cf477313
parent 6180 99f107fd478f
child 6317 128e592f5489
permissions -rw-r--r--
removed use.ML;
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";
6134
ec6092b0599d added General/graph.ML: generic direct graphs;
wenzelm
parents: 6116
diff changeset
     8
use "graph.ML";
5018
ce8e87fad843 General tools.
wenzelm
parents:
diff changeset
     9
use "object.ML";
ce8e87fad843 General tools.
wenzelm
parents:
diff changeset
    10
use "seq.ML";
ce8e87fad843 General tools.
wenzelm
parents:
diff changeset
    11
use "name_space.ML";
ce8e87fad843 General tools.
wenzelm
parents:
diff changeset
    12
use "position.ML";
ce8e87fad843 General tools.
wenzelm
parents:
diff changeset
    13
use "path.ML";
ce8e87fad843 General tools.
wenzelm
parents:
diff changeset
    14
use "file.ML";
5040
78abd4c4802a added General/history.ML;
wenzelm
parents: 5018
diff changeset
    15
use "history.ML";
6116
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents: 5864
diff changeset
    16
use "scan.ML";
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents: 5864
diff changeset
    17
use "source.ML";
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents: 5864
diff changeset
    18
use "symbol.ML";
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents: 5864
diff changeset
    19
use "pretty.ML";
5864
30b6a3251813 prefixed op;
wenzelm
parents: 5040
diff changeset
    20
30b6a3251813 prefixed op;
wenzelm
parents: 5040
diff changeset
    21
structure PureGeneral =
30b6a3251813 prefixed op;
wenzelm
parents: 5040
diff changeset
    22
struct
30b6a3251813 prefixed op;
wenzelm
parents: 5040
diff changeset
    23
  structure Symtab = Symtab;
6136
166b3353aad5 structure Graph = Graph;
wenzelm
parents: 6134
diff changeset
    24
  structure Graph = Graph;
5864
30b6a3251813 prefixed op;
wenzelm
parents: 5040
diff changeset
    25
  structure Object = Object;
30b6a3251813 prefixed op;
wenzelm
parents: 5040
diff changeset
    26
  structure Seq = Seq;
30b6a3251813 prefixed op;
wenzelm
parents: 5040
diff changeset
    27
  structure NameSpace = NameSpace;
30b6a3251813 prefixed op;
wenzelm
parents: 5040
diff changeset
    28
  structure Position = Position;
30b6a3251813 prefixed op;
wenzelm
parents: 5040
diff changeset
    29
  structure Path = Path;
30b6a3251813 prefixed op;
wenzelm
parents: 5040
diff changeset
    30
  structure File = File;
30b6a3251813 prefixed op;
wenzelm
parents: 5040
diff changeset
    31
  structure History = History;
6116
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents: 5864
diff changeset
    32
  structure Scan = Scan;
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents: 5864
diff changeset
    33
  structure Source = Source;
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents: 5864
diff changeset
    34
  structure Symbol = Symbol;
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents: 5864
diff changeset
    35
  structure Pretty = Pretty;
5864
30b6a3251813 prefixed op;
wenzelm
parents: 5040
diff changeset
    36
end;