**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`.

Fri Sep 5 16:28:58 MDT 1997