This manual is a reference manual for version 4.1 of the Nuprl system. It is aimed at beginning and intermediate users of the system. Version 4.1 runs on Unix-based workstations that use the X window system.
Note that this manual is still under development and is incomplete. Most importantly, it is missing information on Nuprl 's type theory, and the structure of the primitive rules as perceived by users when executing low-level tactics.
Information on the ML language can be found in a separate Nuprl ML manual . Tutorials on the use of Nuprl 's term and proof editor are also available.