Future extensions of the system will include a treatment of hiding [7], a uniform treatment of different logics based on the notion of heterogenous development graphs [6], and the maintenance of theory-specific control information for theorem provers. The latter comprises a management for building up the database of theorem provers by demand rather than providing all available axioms and lemmata at once as well as the management of meta-level information, like tactics or proof plans, inside MAYA.