Basic Control Structures

Sequencing:

The term thm_5 => thm_4 => thm_3 => thm_2 => thm1 => term, when ``executed'' will apply the theorems or tactics numbered 1 through 5, in that order, to the original term.

Alternation:

The term thm_5 =>> thm_4 =>> thm_3 =>> thm_2 =>> thm_1 => term, when ``executed'', will apply the first of the theorems or tactics numbered 1 through 5 (as above, in that order, working from the inside out) which applies to the term. No more than one of the tactics will be applied. In principle, the sequencing construction could be used for this as well, if one were certain that applying one of the tactics would not give a form to which one of the later tactics in the list might unexpectedly apply.

Conditionals:

All conditional execution in the tactic language depends on the fact that a theorem is not applied if it does not match its target. The termination of recursive tactics, for example, depends on this.

Guarded commands using *> and <*:

The term (thm_n *> guard_n) =>> ... (thm_1 *> guard_1) => term will apply the first of the theorems guard_i which apply to the term, and then will further apply thm_i. An advantage of this is that thm_i might be constructed using sequencing on a very general term, and so might apply under much more general circumstances than those specified by applicability of guard_i; before this construction was available, it would have been necessary to construct a new theorem with the effect of each composite thm_i *> guard_i.