**exportthm**- ``exportthm view prefix theorem remote-theory''
exports ``theorem'' and all iteratively embedded theorems to
``remote-theory'', using ``view'' to set up the translation, and
adding ``prefix'' to each theorem name. If the view does not check,
no changes will be made. ``#'' is used as the default prefix for
operators which are created during the export. ``remote-theory'' must
be on the desktop.
**exportthmlist**- ``exportthmlist view prefix1 prefix2 theorems
remote-theory'' is a more general version of exportthm above: the
differences are that ``theorems'' is a list of theorems to be
exported, and that prefix1 (for theorem and constant names) is
supplemented with prefix2 (for operator names).

Fri Sep 5 16:28:58 MDT 1997