TRANSFER-LINES : MEXPRTRANSFER-LINES is a top-level command.
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
TPS documentation homepage