INTRODUCE-GAP : MEXPR

INTRODUCE-GAP is a top-level command.
Introduce a gap in an existing proof.
The command format for INTRODUCE-GAP is:

 <n>INTRODUCE-GAP       LINE      NUM 
"EXISTING-LINE" "POSINTEGER"


The arguments have the following meaning:
LINE : Line where gap is to be introduced
NUM : Increment

TPS documentation homepage


© 1988-99, Carnegie Mellon University.

TPS homepage