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