DIY-L : MEXPRDIY-L is a top-level command.
DIY for lemmas. Behaves as for DIY, but puts all new lines into
a specified range rather than scattering them throughout the proof.
The command format for DIY-L is:
<n>DIY-L GOAL SUPPORT WINDOW RANGE
"PLINE" "EXISTING-LINELIST" "YESNO" "LINE-RANGE"
The arguments have the following meaning:
GOAL : Planned Line
SUPPORT : Support Lines
WINDOW : Open Vpform Window?
RANGE : Line range for new lines?
TPS documentation homepage