src/Tools/README

tuned messages -- prefer quote before Position.here, which might be just \<here>;

                 Tools: generic tools outside of Pure

This directory contains ML sources of generic tools.  Typically, they
can be applied to various logics.