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:

<n>NAT-ETREE PREFIX

"SYMBOL"

The arguments have the following meaning:

PREFIX : Name of the Proof

© 1988-99, Carnegie Mellon University.