USE-TACTIC : MEXPR

USE-TACTIC is a top-level command.
Use a tactic on the current goal. The default tactic
is given by the flag DEFAULT-TACTIC.
The command format for USE-TACTIC is:

 <n>USE-TACTIC      TAC    TAC-USE    TAC-MODE 
"TACTIC-EXP" "TACTIC-USE" "TACTIC-MODE"


The arguments have the following meaning:
TAC : Tactic name/expression
TAC-USE : Use
TAC-MODE : Mode

TPS documentation homepage


© 1988-99, Carnegie Mellon University.

TPS homepage