A theorem has an additional component not found in a proof environment: this is a list of subsidiary theorems visible only to the parent theorem. The intended use of this feature is to make it possible to avoid cluttering the theorem list with subcommands of tactics.
The pushtheorem command allows one to ``hide'' one theorem in another. It automatically comments the ``pushed'' theorem so that one can tell where it is (it ceases to be visible on the master theorem list). The poptheorem command allows one to retrieve a theorem, also posting an automatic comment. Variants pushtheorem2 and poptheorem2 do not post comments; this is useful if one is taking a subtactic out of a module in order to edit it, for example.
A theorem with subsidiary theorems is referred to as a ``module''. Modules can be nested. Theorems inside a module are only available when the parent theorem is being executed; be sure that a theorem packed into a module is not needed by any theorem other than its parent theorem or other theorems in the module! Their names are still reserved.
The forget command will eliminate an entire module if any component depends on the theorem being forgotten. Theorem export will work correctly in the presence of modules, but it will not export module structure; exported modules will be completely unpacked.