RESTOREPROOF : MEXPRRESTOREPROOF is a top-level command.
Reads a natural deduction proof from a file created by SAVEPROOF
and makes it the current proof. A security feature prevents the
restoration of saved proofs which have been altered in any way.
Retrieve any definitions which are used in the proof and stored in the
library before restoring the proof. If you don't specify a directory,
it will first try your home directory and then all the directories
listed in SOURCE-PATH.
The command format for RESTOREPROOF is:
The arguments have the following meaning:
SAVEFILE : File in which proof resides
TPS documentation homepage