# HG changeset patch
# User wenzelm
# Date 961969547 -7200
# Node ID 8ca79837b41bce39f5af4e9effdc6cda4f0d0b93
# Parent  62367f8fef02125ab9e7cd604b521909fb821048
tuned;

diff -r 62367f8fef02 -r 8ca79837b41b src/Pure/General/README
--- a/src/Pure/General/README	Sun Jun 25 23:45:26 2000 +0200
+++ b/src/Pure/General/README	Sun Jun 25 23:45:47 2000 +0200
@@ -9,6 +9,7 @@
   Symtab        (tables indexed by strings)
   GraphFun	(generic directed graphs)
   Graph		(graphs indexed by strings)
+  LeftistHeap	(heaps over linearly ordered types)
   Object        (generic objects of arbitrary type)
   Seq           (unbounded sequences)
   NameSpace     (hierarchically structured name spaces)
@@ -22,6 +23,3 @@
   Buffer	(simple string buffers)
   History       (histories of values, with undo and redo)
   Pretty        (generic pretty printing module)
-
-Functor LeftistHeap implements heaps, which are used for best-first search.
-It must be instantiated with a linearly ordered type.
diff -r 62367f8fef02 -r 8ca79837b41b src/Pure/General/ROOT.ML
--- 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";