Translate a ND proof to an eproof and back again

(into a proof with a new name) in the hope of tidying it up a

bit. Equivalent to

NAT-ETREE; MATE ! ; PROP-MSEARCH ; MERGE-TREE ; LEAVE ;

ETREE-NAT ; CLEANUP ; SQUEEZE

The command format for TIDY-PROOF is:

<n>TIDY-PROOF OLD-PRFNAME NEW-PRFNAME

"SYMBOL" "SYMBOL"

The arguments have the following meaning:

OLD-PRFNAME : Name of old proof

NEW-PRFNAME : Name for new proof

© 1988-99, Carnegie Mellon University.