SAVE-SUBPROOF : MEXPR

SAVE-SUBPROOF is a top-level command.
Saves part of the current natural deduction proof to
the specified file in a form in which it can be restored.
The line ranges specified will be increased to include all the
other lines on which the given lines depend. See the help
message for LINE-RANGE to find out what a line-range should
look like. An example list is: 1--10 15--23 28 34--35
Also creates a new proof in memory with the given name, and
makes that the current proof.
Use RESTOREPROOF to restore the proof.
Overwrites the file if it already exists.
The command format for SAVE-SUBPROOF is:

 <n>SAVE-SUBPROOF  SAVEFILE       LINES   SUBNAME 
"FILESPEC" "LINE-RANGE-LIST" "SYMBOL"


The arguments have the following meaning:
SAVEFILE : File in which to save proof
LINES : List of line ranges to save
SUBNAME : Name for new subproof

TPS documentation homepage


© 1988-99, Carnegie Mellon University.

TPS homepage