List Scanning Commands

This subsection describes a family of commands for viewing various kinds of lists in the prover. Each of these commands puts one in an environment with the following one-letter commands:

l

``left'' - go to the item with alphabetically previous label.

r

``right'' - go to the item with alphabetically next label.

Enter

view this item.

q

quit.

h (or any other key)

``help'' - see a list of commands.

The commands available include scandecs (declarations), scanprograms (functional program bindings), scantheorems (theorems), scanenvs (saved proof environments), scantheories (theories on desktop).