# HG changeset patch
# User wenzelm
# Date 918055693 -3600
# Node ID e40b647fd6d02700523239898e659d072dd58355
# Parent  d6d6bdfe83400b95bc42d8fa6de3bacab6d5fbc7
added Use;

diff -r d6d6bdfe8340 -r e40b647fd6d0 src/Pure/General/README
--- a/src/Pure/General/README	Wed Feb 03 16:27:36 1999 +0100
+++ b/src/Pure/General/README	Wed Feb 03 16:28:13 1999 +0100
@@ -20,3 +20,4 @@
   Source        (co-algebraic data sources)
   Symbol        (generalized characters)
   Pretty        (generic pretty printing module)
+  Use		(enhanced ML 'use' command)