EXPUNGE : MATEOPEXPUNGE is a mating-search command.
Frees up space by getting rid of all expansion proofs and option
trees. If you only want to get rid of old expansion proofs and
option trees, you can use EXPUNGE-OLD to do you job.
Warning : After using EXPUNGE, many commands such as ETD, VP, ...,
don't work until you re-initialize the current expansion proof by using
commands such as SUB, MATE, ...
The command format for EXPUNGE is:
TPS documentation homepage