MONSTRO : MEXPRMONSTRO 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:
The arguments have the following meaning:
TACMODE : Mode
TPS documentation homepage