TIDY-PROOF : MEXPR

TIDY-PROOF is a top-level command.
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

TPS documentation homepage


© 1988-99, Carnegie Mellon University.

TPS homepage