A flag setting for TACUSE.

Use tactics in etree-nat translation style (i.e. apply them to the

current eproof to create lines of a natural deduction proof).

Translates the current expansion proof, which is value of internal

variable current-eproof, into a natural deduction style proof. The default

value of the tactic is given by the flag DEFAULT-TACTIC.

The command format for ETREE-NAT is:

<n>ETREE-NAT PREFIX NUM TAC MODE

"SYMBOL" "LINE" "TACTIC-EXP" "TACTIC-MODE"

The arguments have the following meaning:

PREFIX : Name of the Proof

NUM : Line Number for Theorem

TAC : Tactic to be Used

MODE : Tactic Mode

© 1988-99, Carnegie Mellon University.