As explained in detail in Chapter 
, tactics are ML
functions which enable one to automate application of primitive rules.
A simplified but conceptually useful idea of a tactic, is as a function
mapping proofs to proofs. If one applies a tactic in ML to an
unrefined proof and the tactic doesn't fail, then the tactic returns a
proof built (usually) from primitive rules with 0 or more unrefined
leaves.
We give a description of what a tactic rule is, and what happens
when a tactic is executed as a refinement rule. Assume that a proof
editor window is viewing some proof node 
and that
one enters TacticText, the text of some suitable tactic as the
refinement rule.
. Let
the resulting proof term be p. Note that the root goal of p is
always the same as g.
. Rather
it is stored in a tactic rule
along with the ML text of
the tactic. Let us represent the tactic rule by the term
tactic_rule
.
is 
Here, 
, and 
are all the unrefined leaf
nodes of the proof p in the same left-right order as they occur
in p.
The tactic rule hides the proof tree p. When one views a proof term, or a tactic rule refinement, one only ever sees the text of the tactic. From a logical point of view, it is not strictly necessary to keep p around at all, after the tactic has executed. However, it is necessary for extraction purposes.
In the event that a tactic is applied as a refinement rule to an already refined proof term, the proof term is first changed to an unrefined proof, discarding the existing refinement rule and all the sub-proofs, before it is passed to the tactic.
Running a tactic as a refinement rule makes it appear in a proof as a high level rule of inference, and consequently greatly increases the readability of proofs.
The TacticText is represented as an !ml_text alternating sequence and has structure identical to that of ML library objects.