ETREE-NAT : INFO

ETREE-NAT is a flag setting or other piece of information.
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).

TPS documentation homepage


ETREE-NAT : MEXPR

ETREE-NAT is a top-level command.
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

TPS documentation homepage


© 1988-99, Carnegie Mellon University.

TPS homepage