The denotation of a term `thm => term` is the same as the
denotation of the term `term`. `thm` is expected to denote a
theorem which will be applied as a rewrite rule to `term` when the
tactic interpreter `execute` or the tactic debugger `steps`
are invoked. If it turns out that the left side of `thm` does not
match the structure of `term`, its ``application'' will have no
effect on the presentation of `term`.

The denotation of `thm <= term` is similar, except that the
theorem `thm` is to be applied in the opposite sense (when `
term` matches the right side of the equation represented by `
thm` rather than the left side).

In both cases, the rule is applied only at the top level of `
term`; it is not applied to proper subterms.

The prover commands `ruleintro`, `revruleintro` are used to
introduce an application of a theorem (given as the argument of the
command) to the selected subterm of the right side of the current
equation. The prover command `droprule` will eliminate a theorem
application at the top level (this works for all four infixes).

See above for relaxation of stratification rules where embedded theorem applications are involved.

Fri Sep 5 16:28:58 MDT 1997