Environment Display Commands

look

View the whole term (above) and the current subterm (below) (walk command ``?'').

lookback

View the left side of the current equation.

lookhere

View the current subterm alone.

lookhyp

``lookhyp integer'' displays the hypothesis indexed by ``integer''; see the discussion of the hypothesis function of the prover above.

lookhyps

Displays all hypotheses.

seedeps

See the dependencies of the theorem under construction. (walk command ``j'').