diff -r 0bc590051d95 -r a5db2f7d7654 src/Tools/README
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/README	Thu May 31 12:59:31 2007 +0200
@@ -0,0 +1,8 @@
+
+                 Tools: generic tools outside of Pure
+
+This directory contains ML sources of generic tools.  Typically, they
+can be applied to various logics.
+
+
+$Id$