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.

Fri Sep 5 16:28:58 MDT 1997