CREATE-SUBPROOF : MEXPR

CREATE-SUBPROOF is a top-level command.
Creates a new proof in memory from the given lines,
plus all the lines on which they depend, and makes that
the current proof.
The command format for CREATE-SUBPROOF is:

 <n>CREATE-SUBPROOF       LINES  SUBNAME 
"LINE-RANGE-LIST" "SYMBOL"


The arguments have the following meaning:
LINES : List of line ranges to use
SUBNAME : Name for new subproof

TPS documentation homepage


© 1988-99, Carnegie Mellon University.

TPS homepage