NAT-ETREE-OLD : MEXPRNAT-ETREE-OLD is a top-level command.
Translates a natural deduction proof into an expansion proof
using the old method. The default value is the name of the current proof,
namely the value of DPROOF.
The command format for NAT-ETREE-OLD is:
The arguments have the following meaning:
PREFIX : Name of the Proof
TPS documentation homepage