CLEANUP : MEXPR

CLEANUP is a top-level command.
If the proof is complete, will delete unnecessary lines
from a proof. It may also eliminate or suggest eliminating
unnecessary hypotheses.
If the proof is incomplete, will do a partial cleanup in which
only unnecessary lines justified by SAME will be removed.
The command format for CLEANUP is:

 <n>CLEANUP 

TPS documentation homepage


© 1988-99, Carnegie Mellon University.

TPS homepage