EXPUNGE : MATEOP

EXPUNGE 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:

<Mate>EXPUNGE

TPS documentation homepage


© 1988-99, Carnegie Mellon University.

TPS homepage