GO2 : MEXPR

GO2 is a top-level command.
Apply all possible invertible tactics, until no more are possible.
This is equivalent to typing USE-TACTIC GO2-TAC NAT-DED.
The amount of output to the main window and the proofwindows is
determined by the flag ETREE-NAT-VERBOSE.
The command format for GO2 is:

 <n>GO2    TACMODE 
"TACTIC-MODE"


The arguments have the following meaning:
TACMODE : Mode

TPS documentation homepage


© 1988-99, Carnegie Mellon University.

TPS homepage