Tools: generic tools outside of Pure This directory contains ML sources of generic tools. Typically, they can be applied to various logics. $Id$