The library facility in Nuprl also allows one to save theorems, definitions and other objects produced in a session. For example, if it were desired to save the theorem t1 of the previous example in a file named library-name, one would issue the command
dump t1 to library-name.The theorem (together with its proof, if it has been proved) is stored in the file named in the dump command. If there is a library of several objects, say
#t1
THM ...
#t2
THM
.
.
#tn
THM
then the entire library can be saved by the command
dump t1-tn to library-nameor by the command
dump first-last to library-name.Any segment of a library, say t5 to t9, can be saved by the command
dump t5-t9 to library-name.If one later wishes to retrieve a stored library, one issues the command
load place from library-name,where place refers to a place in the active system library and may be either top, bottom, before name or after name.