This section discusses the management of theories and environments other than the current one, whether saved on the desktop or in files. It also discusses theory interpretations and their use in the theorem export facility which allows results proved in one theory to be exported to another.