Also see Nuprl4 Lib for newer material.

next up previous contents index
Next: Basic Definitions Up: No Title Previous: Theories

Mathematics Libraries

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.)

Richard Eaton
Thu Sep 14 08:45:18 EDT 1995