To invoke a transformation tactic at some node of a proof, position a proof editor window at that node and use the TRANSFORM command . This opens up a transformation-tactic window and initializes it to take tactic text. Type the name of the tactic and any arguments into the window and then use the EXIT term editor command. Nuprl will apply the tactic and redisplay the proof window to show any effects. If the expression entered doesn't parse or typecheck, a diagnostic message is printed and the window is left as is. If the tranformation tactic fails, the proof is left unchanged.