next up previous contents
Next: Command Abbreviations Up: Appendix: Reference for Individual Previous: View Management Commands

Theorem Export Commands

``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 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).

Randall Holmes
Fri Sep 5 16:28:58 MDT 1997