The main directories containing theories are listed in
Section 
. Each theory directory contains an ML
file theory-init.ml
. This file contains commands that tell
Nuprl
about the theories in the theory directory, including
information about the dependencies of theories on one another. It also
should contain comments that summarize the contents of each theory in
the directory.
Theory directories should also contain up-to-date listings of each theory. Short listings are named theory-name .prl and long listings containing printouts of proofs are named theory-name _long.prl . These listings use characters from Nuprl 's 8-bit character set and so are best viewed using an editor running with one of Nuprl 's fonts. There are also self-contained LaTeX versions of the listings in files with .tex rather than .prl file-name extensions .
ML commands for creating, loading, editing, dumping and printing
theories are described in Section
.