Abstract
For reasoning about large and complex systems, proof tools should provide sophisticated theory structuring facilities, just as programming languages should provide module facilities in order to support programming in-the-large. This paper describes a set of theory structuring facilities that supports theory reuse effectively, provides separate name spaces and independent syntax for each theory, and fully supports interpretation and instantiation of theories. These facilities have been implemented in the Ergo 4.1 proof tool.