next up previous contents
Next: Finishing Up Up: The Proof Environment Previous: Local Term Manipulation

Global Variable Assignment

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.

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