This chapter contains brief descriptions of
some of the libraries which have been built
with Nuprl. The accounts are intended to convey the flavor of various kinds
of formalized mathematics.
In much of the presentation which
follows the theorems, definitions and proofs shown
are not exactly in the form that would be displayed on the screen
by Nuprl
, although they come from actual Nuprl
sessions (via the
snapshot feature). The
theorems (anything
starting with ``` >>`'') will have some white space (i.e.,
carriage returns and blanks) added, while
the DEF objects will have additional white space as well as
escape characters and many of the parentheses omitted.
(Usually the right--hand sides of definitions have seemingly
redundant parentheses; these ensure correct parsing in
any context.)

Thu Sep 14 08:45:18 EDT 1995