# HG changeset patch
# User wenzelm
# Date 1131550007 -3600
# Node ID 0e9c9a18f454343982fd0e444ddb8e0c0bb14134
# Parent  8c3089df74baef30708c608c313cb4f9741833bb
tuned comments;

diff -r 8c3089df74ba -r 0e9c9a18f454 src/Pure/General/ROOT.ML
--- a/src/Pure/General/ROOT.ML	Wed Nov 09 16:26:46 2005 +0100
+++ b/src/Pure/General/ROOT.ML	Wed Nov 09 16:26:47 2005 +0100
@@ -1,7 +1,7 @@
 (*  Title:      Pure/General/ROOT.ML
     ID:         $Id$
 
-Library of general tools --- prefer this over the 'Standard ML Library'.
+Library of general tools.
 *)
 
 use "stack.ML";
diff -r 8c3089df74ba -r 0e9c9a18f454 src/Pure/General/buffer.ML
--- a/src/Pure/General/buffer.ML	Wed Nov 09 16:26:46 2005 +0100
+++ b/src/Pure/General/buffer.ML	Wed Nov 09 16:26:47 2005 +0100
@@ -2,7 +2,7 @@
     ID:         $Id$
     Author:     Markus Wenzel, TU Muenchen
 
-Simple string buffers.
+Efficient string buffers.
 *)
 
 signature BUFFER =