This paper describes TML, a metalanguage intended for proof development and program design environments. The abstract theory and meta-module mechanisms are presented in TML to allow a good modularization of proof development and make it possible to direct the search for a proof in well-structured theories mechanically.