Whereas refinement tactics take only goals as arguments and return proofs, transformation tactics take proofs as arguments and return proofs. Transformation tactics can perform much more global analysis and change to proofs than can refinement tactics. These tactics, for instance, can complete or expand an unfinished proof, produce a new proof that is analogous to the given proof and perform various optimizations to the proof such as replacing subproofs with more elegant or concise ones, to name a few of the uses to which they have been put.
A user invokes a transformation tactic by editing the theorem of
interest and traversing the proof until the goal heading the desired
subproof is displayed. The user then types 
, and
will prompt
for the name of the transformation tactic which is to be applied. The tactic
is applied to the proof consisting of the current goal and anything that
is below it, that is, any subgoals and proofs below the subgoals. The
transformation tactic, if it succeeds, will return a proof which has the
same goal as the argument proof tree. Unlike those of
refinement tactics, the name
of the transformation tactic is not entered into the proof; the tactic
serves as an operation on proofs, transforming one proof to another.
Upon termination the proof returned may bear little resemblance to the
original proof, except that a transformation tactic cannot change the proof
above the root of the argument, nor can it change the goal of the root of
the subproof. The only exception to this rule is if the subproof is the
whole proof---the tactic was called from the top goal. In this case the
transformation tactic may replace the goal of the proof; thus a
transformation tactic can map one theorem into another. These constraints
are enforced by the implementation and need not be the concern of the
tactic designer or user.