The operators `*>` and `<*` are binary operators on theorems;
the result of the application of `thm1 *> thm2`, for example, is
that `thm2` is applied (in the usual direction) and then `
thm1` is applied if the application of `thm2` succeeded.

The unary operator `!!` functions as a kind of ``inlining''
operator. The success or failure of application reported by `
!!thm => term` is either failure if `thm` does not apply (this
operator should normally be used with theorems which do not fail) or
the success or failure of the last embedded theorem application at the
top level of the term which results from the application of `thm`.
The typical use of this is in case `thm` is of the form

?x = (thm1 => thm2 => ... thmn => ?x);such a theorem is always applicable (and clearly true) and has the effect of causing a sequence of theorems to be applied; success/failure of

The on-success commands can be used for building guarded lists of
commands to be executed; the inlining operator is provided to make
certain kinds of defined operations on theorems behave sensibly. They
do not interact with each other too well: theorems of the form `
(!! thm2) *> thm1` or `thm2 *> (!! thm1)` do not work in any
useful way, but a theorem of the form `!!(thm2 *> thm1)` will work
as expected. The problem is that the notion of success/failure is
determined in different ways by the infixes `*>` and `<*` on
the one hand and the inlining operator on the other. Using the
criterion used by the guard infixes, the application of an inlined
theorem *always* succeeds, though this may not be what the inlined
theorem may report to a following theorem.

An equation `term1 = term2` can be applied as an embedded theorem;
the tactic interpreter will search for a theorem which justifies the
equation, and apply such a theorem if it finds it. This is useful if
one has forgotten the name of a theorem whose form one knows; more
powerful possibilities arise from this, since it allows the tactic
interpreter to construct possible theorems ``dynamically''.

Fri Sep 5 16:28:58 MDT 1997