**right**- Changes current subterm to right subterm of previous
current subterm. Takes the immediate proper subterm of a constant
function term (walk command ``r'').
**left**- Changes current subterm to left subterm of previous
current subterm. Takes the immediate proper subterm of a constant
function term (walk command ``l'').
**up**- Changes current subterm to the smallest subterm properly
including the previous current subterm (walk command ``u'').
**top**- Changes current subterm to the whole term (walk command ``t'').
**upto**- ``upto term'' repeats ``up'' until a term is encountered
which matches ``term'' in structure, or until the whole term is
reached. (walk command ``o'')
**downtoleft**- ``downtoleft term'' goes to the leftmost term
matching ``term'' in structure. (walk command ``<'')
**downtoright**- As ``downtoleft'', except rightmost. (walk command ``>'')
**New movement commands:**- Commands
`uptols <theorem>`,`uptors <theorem>`,`dlls <theorem>`,`dlrs <theorem>`,`drrs <theorem>`, and`dlrs <theorem>`enable movement to places where theorems can be applied. Commands beginning with`upto-`implement ``upto''; commands beginning with`dr-`and`dl-`implement ``downtoleft'' and ``downtoright''; the suffix indicates ``left side'' or ``right side'' of theorem.

Fri Sep 5 16:28:58 MDT 1997