View management and theorem export:

declareview:

This command takes a single string argument. A new view is declared, named by the argument, translating all predeclared constants and operators to themselves.

restoreview:

This command takes a single string argument. The view named by the argument is restored from a backup view (backup views are saved by exportthm). To be used when an export fails.

backupview:

This command takes a single string argument. A backup view is created for the view named by the argument.

addtoview:

This command takes three string arguments. It adds a line to a view's translation table: the second argument (a constant or operator) is to be translated by the third argument (a constant or operator) in the view named by the first argument.

dropfromview:

This command takes two string arguments. It drops the translation of the second argument (if any) from the view named by the first argument.

dropview:

This command erases the view named by its single string argument (if any).

exportthm:

This command takes four string arguments. The first is a view. The second is the name of a theory on the desktop. The third is a suffix to be used to modify names of constants to avoid name collision (# is always used as a prefix to modify names of operators to avoid name collisions). The last is the name of a theorem in the current theory. The command cosntructs the list of theorems which need to be exported to export the theorem argument, moves to the remote theory argument, checks and extends the view as needed to carry out the export, then translates the list of theorems. This command may be somewhat unstable; it seems to work and to be much faster than it was under Mark2.

[declareview:] This command takes a single string argument. A new view is declared, named by the argument, translating all predeclared constants and operators to themselves.

[restoreview:] This command takes a single string argument. The view named by the argument is restored from a backup view (backup views are saved by exportthm). To be used when an export fails.

[backupview:] This command takes a single string argument. A backup view is created for the view named by the argument.

[addtoview:] This command takes three string arguments. It adds a line to a view's translation table: the second argument (a constant or operator) is to be translated by the third argument (a constant or operator) in the view named by the first argument.

[dropfromview:] This command takes two string arguments. It drops the translation of the second argument (if any) from the view named by the first argument.

[dropview:] This command erases the view named by its single string argument (if any).

[exportthm:] This command takes four string arguments. The first is a view. The second is the name of a theory on the desktop. The third is a suffix to be used to modify names of constants to avoid name collision (# is always used as a prefix to modify names of operators to avoid name collisions). The last is the name of a theorem in the current theory. The command cosntructs the list of theorems which need to be exported to export the theorem argument, moves to the remote theory argument, checks and extends the view as needed to carry out the export, then translates the list of theorems. This command may be somewhat unstable; it seems to work and to be much faster than it was under Mark2.