... In Task T3.4 we will add in new theory management facilities to
suppport the sharing of proof-related data among the CAD/CASE tools,
the plug-ins, and the core proof engine. The core prover API will
... be upgraded, ... so that it supports the theory-related
requirements of the client tools and the plug-ins. This upgrade
requires concomitant changes and improvements to the current theory
management scheme used in HOL, which is slanted towards interactive
use. In particular, we aim to track dependency relationships between
proofs and between theories, so that theory revision can be
automated. Also we envision that multiple and simultaneous theory
contexts are needed to support the requirements of the CAD/CASE
tools.
The result of this task will be a theory management subsystem that
will support the flow of large quantities of theory-related data
among the CAD/CASE tools, the plug-ins, and the core proof
system. Also, it will support the tracking and maintenance of
theory-related information for the client tools.
(Internal PROSPER document)