src/Pure/General/ROOT.ML
author paulson
Fri, 18 Feb 2000 15:35:29 +0100
changeset 8255 38f96394c099
parent 6644 123b215882ae
child 9095 3b26cc949016
permissions -rw-r--r--
new distributive laws
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";
6634
6f74e7aa5b4d moved scan.ML;
wenzelm
parents: 6317
diff changeset
    13
use "scan.ML";
6638
731b4aec2fd6 added url.ML;
wenzelm
parents: 6634
diff changeset
    14
use "source.ML";
731b4aec2fd6 added url.ML;
wenzelm
parents: 6634
diff changeset
    15
use "symbol.ML";
5018
ce8e87fad843 General tools.
wenzelm
parents:
diff changeset
    16
use "path.ML";
6638
731b4aec2fd6 added url.ML;
wenzelm
parents: 6634
diff changeset
    17
use "url.ML";
5018
ce8e87fad843 General tools.
wenzelm
parents:
diff changeset
    18
use "file.ML";
6317
128e592f5489 added Buffer;
wenzelm
parents: 6222
diff changeset
    19
use "buffer.ML";
5040
78abd4c4802a added General/history.ML;
wenzelm
parents: 5018
diff changeset
    20
use "history.ML";
6116
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents: 5864
diff changeset
    21
use "pretty.ML";
5864
30b6a3251813 prefixed op;
wenzelm
parents: 5040
diff changeset
    22
30b6a3251813 prefixed op;
wenzelm
parents: 5040
diff changeset
    23
structure PureGeneral =
30b6a3251813 prefixed op;
wenzelm
parents: 5040
diff changeset
    24
struct
30b6a3251813 prefixed op;
wenzelm
parents: 5040
diff changeset
    25
  structure Symtab = Symtab;
6136
166b3353aad5 structure Graph = Graph;
wenzelm
parents: 6134
diff changeset
    26
  structure Graph = Graph;
5864
30b6a3251813 prefixed op;
wenzelm
parents: 5040
diff changeset
    27
  structure Object = Object;
30b6a3251813 prefixed op;
wenzelm
parents: 5040
diff changeset
    28
  structure Seq = Seq;
30b6a3251813 prefixed op;
wenzelm
parents: 5040
diff changeset
    29
  structure NameSpace = NameSpace;
30b6a3251813 prefixed op;
wenzelm
parents: 5040
diff changeset
    30
  structure Position = Position;
6634
6f74e7aa5b4d moved scan.ML;
wenzelm
parents: 6317
diff changeset
    31
  structure Scan = Scan;
6644
wenzelm
parents: 6638
diff changeset
    32
  structure Source = Source;
6638
731b4aec2fd6 added url.ML;
wenzelm
parents: 6634
diff changeset
    33
  structure Symbol = Symbol;
5864
30b6a3251813 prefixed op;
wenzelm
parents: 5040
diff changeset
    34
  structure Path = Path;
6638
731b4aec2fd6 added url.ML;
wenzelm
parents: 6634
diff changeset
    35
  structure Url = Url;
5864
30b6a3251813 prefixed op;
wenzelm
parents: 5040
diff changeset
    36
  structure File = File;
6317
128e592f5489 added Buffer;
wenzelm
parents: 6222
diff changeset
    37
  structure Buffer = Buffer;
5864
30b6a3251813 prefixed op;
wenzelm
parents: 5040
diff changeset
    38
  structure History = History;
6116
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents: 5864
diff changeset
    39
  structure Pretty = Pretty;
5864
30b6a3251813 prefixed op;
wenzelm
parents: 5040
diff changeset
    40
end;