NAT-ETREE is a top-level command.
Translates a natural deduction proof, (which must be the current dproof
-- use RECONSIDER to return to an old proof in memory), into an
expansion proof. This will not work on all proofs: in particular,
proofs containing ASSERT of anything but REFL= and SYM=, proofs
using rewrite rules and proofs containing SUBST= or SUB= cannot be
translated at present. However, the user is given the option of
removing lines justified by SUBST= or SUB= and replacing the justification
with a subproof. This permanently modifies the proof. (AUTO-SUGGEST
also gives such an option.)
The command format for NAT-ETREE is:


The arguments have the following meaning:
PREFIX : Name of the Proof

TPS documentation homepage

© 1988-99, Carnegie Mellon University.

TPS homepage