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:


TPS documentation homepage

© 1988-99, Carnegie Mellon University.

TPS homepage