MODIFY-GAPS : MEXPRMODIFY-GAPS is a top-level command.
Remove unnecessary gaps from the proof structure, and modify
line numbers so that the length of each gap is neither less than the first
argument, nor greater than the second.
The command format for MODIFY-GAPS is:
<n>MODIFY-GAPS NUM1 NUM2
The arguments have the following meaning:
NUM1 : min length of gap
NUM2 : max length of gap
TPS documentation homepage