PFNAT : MEXPRPFNAT is a top-level command.
To generate a NATREE from given proof and store it in CURRENT-NATREE. This may
evolve into a command for rearranging natural deduction style proofs.
The command format for PFNAT is:
The arguments have the following meaning:
PROOF : Proof to be mapped
TPS documentation homepage