next up previous contents
Next: Tactic Language Interpreter Up: Appendix: Reference for Individual Previous: Rule Introduction Commands

Assignment Commands

assign
``assign variable term'' replaces the variable ``variable'' with the term ``term'' throughout the equation under construction. (walk command ``a'').

assigninto
``assigninto variable term'' replaces the variable ``variable'' with the two sides of the equation under construction to produce a new equation under construction. (walk command ``n'').

assignright
``assignright var thm'' assigns the right side of theorem ``thm'' as the value of the variable ``var'' throughout the current and initial terms of the theorem under construction.

assignleft
As ``assignright'', but the left side of ``thm''.



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