... 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)