Copies all of the given lines of a subproof, and

all lines on which they depend, 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).

Different comments from two otherwise identical lines will be

concatenated to form the comment in the resulting proof.

This is equivalent to CREATE-SUBPROOF followed by MERGE-PROOFS.

The following proofs are in memory:

For more details, use the PROOFLIST command.

The command format for TRANSFER-LINES is:

<n>TRANSFER-LINES PROOF SUBPROOF LINES

"SYMBOL" "SYMBOL" "LINE-RANGE-LIST"

The arguments have the following meaning:

PROOF : Name of main proof

SUBPROOF : Name of proof to transfer lines from

LINES : Range of lines to transfer

© 1988-99, Carnegie Mellon University.