equal
deleted
inserted
replaced
1 (* Title: Pure/General/ROOT.ML |
1 (* Title: Pure/General/ROOT.ML |
2 ID: $Id$ |
2 ID: $Id$ |
3 |
3 |
4 General tools. |
4 Library of general tools --- prefer this over the 'Standard ML Library'. |
5 *) |
5 *) |
6 |
6 |
7 use "heap.ML"; |
|
8 use "table.ML"; |
7 use "table.ML"; |
9 use "graph.ML"; |
8 use "graph.ML"; |
|
9 use "heap.ML"; |
10 use "object.ML"; |
10 use "object.ML"; |
11 use "seq.ML"; |
11 use "seq.ML"; |
12 use "name_space.ML"; |
12 use "name_space.ML"; |
13 use "position.ML"; |
13 use "position.ML"; |
14 use "scan.ML"; |
14 use "scan.ML"; |