next up previous contents index
Next: The Text Editor Up: Libraries Previous: Entry of Objects

Saving Results


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

then the entire library can be saved by the command
        dump t1-tn to library-name
or 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.

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