Theories

  Closely related theorems, definitions, and comments in Nuprl are grouped into theories. Theories occupy contiguous sections in the library, and are delimited by easily-identified comment objects. Usually only a subset of the existing theories are loaded in any one Nuprl session.

You should keep theorems and definitions which you develop in your own theory. We describe how to create a theory, how to save it to a file, how load it into a session, and how to print it. All the functions calls listed in this section should be typed in to the ML Top Loop.