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

Compare TRANSFER-LINES.

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

"SYMBOL" "SYMBOL"

The arguments have the following meaning:

PROOF : Name of main proof

SUBPROOF : Name of subproof to merge into it

© 1988-99, Carnegie Mellon University.