changeset 9119 | 8ca79837b41b |
parent 9095 | 3b26cc949016 |
child 12420 | a2a05c952b4d |
--- a/src/Pure/General/ROOT.ML Sun Jun 25 23:45:26 2000 +0200 +++ b/src/Pure/General/ROOT.ML Sun Jun 25 23:45:47 2000 +0200 @@ -1,12 +1,12 @@ (* Title: Pure/General/ROOT.ML ID: $Id$ -General tools. +Library of general tools --- prefer this over the 'Standard ML Library'. *) -use "heap.ML"; use "table.ML"; use "graph.ML"; +use "heap.ML"; use "object.ML"; use "seq.ML"; use "name_space.ML";