SUBPROOF : MEXPR

SUBPROOF is a top-level command.

Concentrate on proving a particular planned line.
The command format for SUBPROOF is:

 <n>SUBPROOF  PLINE 
"PLINE"


The arguments have the following meaning:
PLINE : Line to prove

TPS documentation homepage


© 1988-99, Carnegie Mellon University.

TPS homepage