tactic.def_replacer
Define a new replaceable tactic.
tactic.def_replacer_cmd
Define a new replaceable tactic.