MERGE-PROOFS : MEXPRMERGE-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:
<n>MERGE-PROOFS PROOF SUBPROOF
The arguments have the following meaning:
PROOF : Name of main proof
SUBPROOF : Name of subproof to merge into it
TPS documentation homepage