Introduction

Nuprl's library is a mathematical and logical database  . The library is composed of objects  . There are objects for theorems and definitions, and also for example objects which control the visual appearance of the mathematical notation. See Section for a list of object types.

Library objects are grouped into theories . Every object belongs to exactly one theory. As yet, there is no nesting of theories. The dependencies of theories on one-another forms a partial order. Within each theory, objects are ordered linearly. The dependencies of library objects on one another is discussed more in Section . Theories are kept in files. In a Nuprl session, one usually loads into the library only those theories that one needs to reference. These theories would include the theories of immediate interest together with the all the ancestors of those theories.

The library window shows information on a segment of the library. The format of the window is discussed in Section . Commands for controlling the library window, editing the library and loading and dumping theories are discussed in Section .

Note that proofs are stored in a compressed format  in files, and expansion of proofs loaded from files is only on demand. Expansion can often be quite slow. See Section for details.