next up previous contents
Next: Declaration Commands Up: Appendix: Reference for Individual Previous: Display Control Commands

Movement Commands

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.



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