Transformation tactics have the same type as normal tactics. However,
they can be run on any node of a proof, not just leaf nodes. Examples
of transformation tactics can be found in
Section 
.
When a transformation tactic is run on a proof p, the proof editor replaces p with the proof resulting from the tactic; it doesn't create a special proof node that just has the unproven subgoals of the resulting proof as its immediate subgoals. Nor is the text of the transformation tactic saved anywhere.