Transformation tactics are tactics which act as proof transformers rather than as generalized refinement rules. To invoke a transformation tactic, press
( in some older versions). This will bring up a text edit window labelled Transformation Tactic. Type the name of the tactic and any arguments into the window and press ;
will call the tactic and redisplay the proof window to show any effects. If the tactic returns an error message it will be displayed in the command/status window.