MERGE-PROOFS is a top-level command.
Merges all of the lines of a subproof into the current
proof. If EXPERTFLAG is NIL, no line number may occur in both proofs.
If EXPERTFLAG is T, then if a line number occurs in both proofs, the
lines to which they refer must be the same (with one exception: if
one is a planned line and the other is the same line with a
justification, then the justified line will overwrite the planned one).

The following proofs are in memory:

For more details, use the PROOFLIST command.

The command format for MERGE-PROOFS is:


The arguments have the following meaning:
PROOF : Name of main proof
SUBPROOF : Name of subproof to merge into it

TPS documentation homepage

© 1988-99, Carnegie Mellon University.

TPS homepage