--- 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";