author | wenzelm |
Sat, 08 Oct 2005 22:39:40 +0200 | |
changeset 17802 | f3b1ca16cebd |
parent 17346 | 2923018471c2 |
child 17848 | de5d9d5e99f5 |
permissions | -rw-r--r-- |
5018 | 1 |
(* Title: Pure/General/ROOT.ML |
2 |
ID: $Id$ |
|
3 |
||
9119 | 4 |
Library of general tools --- prefer this over the 'Standard ML Library'. |
5018 | 5 |
*) |
6 |
||
17346 | 7 |
use "stack.ML"; |
16465 | 8 |
use "ord_list.ML"; |
17152 | 9 |
use "alist.ML"; |
5018 | 10 |
use "table.ML"; |
14831
7c37c18a6188
added Pure/General/output.ML; load Pure/General/pretty.ML early in Pure/ROOT.ML;
wenzelm
parents:
14594
diff
changeset
|
11 |
use "output.ML"; |
16136 | 12 |
use "graph.ML"; |
13 |
use "heap.ML"; |
|
14594
3ff9cfc5c403
Moved symbol.ML to front of file list (due to quote function).
berghofe
parents:
14278
diff
changeset
|
14 |
use "scan.ML"; |
3ff9cfc5c403
Moved symbol.ML to front of file list (due to quote function).
berghofe
parents:
14278
diff
changeset
|
15 |
use "source.ML"; |
3ff9cfc5c403
Moved symbol.ML to front of file list (due to quote function).
berghofe
parents:
14278
diff
changeset
|
16 |
use "symbol.ML"; |
16136 | 17 |
use "name_space.ML"; |
5018 | 18 |
use "seq.ML"; |
19 |
use "position.ML"; |
|
20 |
use "path.ML"; |
|
6638 | 21 |
use "url.ML"; |
5018 | 22 |
use "file.ML"; |
6317 | 23 |
use "buffer.ML"; |
5040 | 24 |
use "history.ML"; |
12420 | 25 |
use "xml.ML"; |