There is a spectrum of assignment commands which make substitutions for variables in a couple of different senses. These commands are unusual in that they can affect the left side of the current equation. The most important use of these commands is in assigning values to new variables introduced by theorem applications; another use for them is in entering large terms.

The `assign`
command takes two terms as parameters and carries out the
substitutions for variables represented by the match of those two
terms (the simplest application is a statement like `assign ?x
?y+?z`, which would replace all occurrences of `?x` with `
?y+?z`. Note that substitutions have to be carried out globally
(not just in the selected term) and in both sides of the current
equation!

The `assigninto` command takes as arguments a free
variable term and a term, and produces a new equation which results
from substituting both sides of the current equation for the free
variable parameter in the term parameter; this implements ``doing the
same thing to both sides of an equation''.

Each of these commands can be suffixed with `-it`, which causes
the last parameter to be set to the selected subterm.

The `assignleft` and `assignright` commands allow one to
assign the left or right side of a theorem to a variable.

Fri Sep 5 16:28:58 MDT 1997