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.