The `applythm` and `applyconvthm` commands can be used to
apply a theorem or its converse to the selected subterm without
invoking the command interpreter. This might sometimes be useful for
editing tactics, for example. The `applyenv` and `
applyconvenv` commands allow similar use of saved environments.

The rule introduction commands `ruleintro`, `revruleintro`,
`altruleintro` and `altrevruleintro` introduce embedded
theorems (given as parameters) connected with `=>`, `<=`, `
=>>`, or `<<=`, respectively. The command `droprule`
removes an embedded theorem. The command `altrule` toggles an
embedded theorem between standard and alternate versions. The commands
`delay` and `undelay` introduce and remove the special delay
operator `#`. The commands `lazy` and `unlazy` introduce
and remove the full laziness prefix `##`.

The special rule introduction commands `matchruleintro` and `
targetruleintro` will introduce a theorem (if there is one) which
matches a given equation or which converts the selected subterm to a
given form, respectively.

The `execute` command invokes the tactic interpreter on the
selected subterm. The `onestep` command carries out one step,
executing all innermost embedded theorems in parallel. The `
steps` command does one step each time the enter key is struck.

Fri Sep 5 16:28:58 MDT 1997