tuned;
authorwenzelm
Sun, 25 Jun 2000 23:45:47 +0200
changeset 9119 8ca79837b41b
parent 9118 62367f8fef02
child 9120 04a46ceace35
tuned;
src/Pure/General/README
src/Pure/General/ROOT.ML
--- 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.
--- 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";