The Nuprl
system provides an
interactive medium
which is accessed via a
screen divided into various windows
and a keyboard/mouse which
allows communication with the system. The windows represent regions of
the system
with specialized roles in the interactive process; the different kinds of
windows are listed in figure
.
Figure: Windows Used in the Nuprl System
The terminal is used to enter definitions, commands, proof steps and so forth into the appropriate window of the system. Commands that allow movement between windows and modification of the view of the environment consist of control sequences or mouse commands. In this section these features are described in as much detail as is needed for the purposes of this chapter. Chapter 7 contains a comprehensive discussion of system features.