The appropriate side of the theorem is matched to the target subterm
and the format of the theorem is matched to the format of the embedded
instance; these matches have to be consistent with one another. If
everything works, the target term is replaced with the appropriate
instance of the other side of the theorem. New variables may be
introduced by this process; such variables have automatically
generated numerical suffixes to reduce the chance of unintended
identifications of new variables with old ones or other new ones. The
command `initializecounter` reinitializes the counter which
provides the automatically generated numerals.

To enforce some degree of confluence, terms containing rule infixes or delay operators do not match anything for purposes of theorem application.

It should also be noted that the tactic interpreters are not applied to terms representing embedded theorems.

Fri Sep 5 16:28:58 MDT 1997