The semantics of the *alternative rule infixes* `=>>` and `
<<=` reflect a need for finer control of the circumstances under
which rules are applied. These should appear only in contexts like
`thm1 =>> thm2 =>> ... thmn =>> firstthm => term`, where the
directions of any arrows that appear can be reversed. Note that the
last rule infix is *not* an alternative infix!

Once `term` becomes free of embedded theorems in the course of the
execution of the tactic interpreter, an attempt is made to apply each
of the theorems in the list, working from the inside out, until one
applies, after which the remaining theorems linked with alternative
infixes are ignored. Lists of alternative theorems linked with the
standard rule infixes have the undesirable feature that more than one
of the theorems might apply in an unexpected way.

The precise way in which this effect is achieved is that a theorem embedded via an alternative infix is executed only if the term to which it is applied is the result of an immediately preceding rewrite rule application at the top level which failed. Once an application succeeds, alternative rule applications are ignored (this will be iterated). This is the reason why the innermost infix must be standard; there is no preceding rule application to consider.

Theorems embedded with alternative infixes can be introduced using
`altruleintro`, `altrevruleintro`. `altrule` can be used
to toggle between alternative and standard infixes.

There is a theoretical inelegance about the alternative rule infixes;
they probably ought to have the same structure as the ``on-sucess''
infixes discussed in the next subsection (i.e., the construction `
?thm1 =>> ?thm2 => term` ought to be `(?thm1 =>> ?thm2) => term`;
the behaviour of the alternative infixes makes the effects of the
tactic interpreters non-local in a way which would be avoided by such
a change. However, non-locality is now pervasive, given variable
binding and local hypotheses, so we are not planning to change this
situation. It is interesting to observe that if the change described
above were made and the precedence of the alternative infixes were set
to 1, there would be no effect on the appearance of terms.

Fri Sep 5 16:28:58 MDT 1997