DIY-L : MEXPR

DIY-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


© 1988-99, Carnegie Mellon University.

TPS homepage