# HG changeset patch
# User wenzelm
# Date 1180609171 -7200
# Node ID a5db2f7d7654d31424d0b91ab3ef0091e9c71e3d
# Parent  0bc590051d957011eea6880b9687276141de98a8
Tools: generic tools outside of Pure.

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$