next up previous contents
Next: Global Variable Assignment Up: The Proof Environment Previous: Term Display

Local Term Manipulation

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.

Randall Holmes
Fri Sep 5 16:28:58 MDT 1997