tuned comments;
authorwenzelm
Wed, 09 Nov 2005 16:26:47 +0100
changeset 18132 0e9c9a18f454
parent 18131 8c3089df74ba
child 18133 1d403623dabc
tuned comments;
src/Pure/General/ROOT.ML
src/Pure/General/buffer.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";
--- 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 =