src/Pure/General/ROOT.ML
changeset 18132 0e9c9a18f454
parent 17848 de5d9d5e99f5
child 18387 90b2b2fd3fdf
--- 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";