MONSTRO : MEXPR

MONSTRO is a top-level command.
This is equivalent to typing USE-TACTIC MONSTRO-TAC NAT-DED.
It applies all the same tactics as GO2, and also ui-herbrand-tac.
The amount of output to the main window and the proofwindows is
determined by the flag ETREE-NAT-VERBOSE.
The command format for MONSTRO is:

 <n>MONSTRO    TACMODE 
"TACTIC-MODE"


The arguments have the following meaning:
TACMODE : Mode

TPS documentation homepage


© 1988-99, Carnegie Mellon University.

TPS homepage