The load and dump commands let one save results between sessions.
writes a representation of the selected objects from the current library to the file. If no filename is given the name of the last file to be loaded is used. The dumped objects are not removed from the library.
Theorem objects are not fully reconstructed. The top of the proof (its goal and status) is loaded, but not the actual body of the proof (the rule applications and subgoals). The body is loaded on demand when the theorem is checked or viewed or when the extractor needs the body of the proof. When the body is actually loaded, the theorem's status is recalculated. If the new status is different from the status the theorem had when it was dumped, a warning is given.
Be sure to keep library objects correctly sorted; if an object a is referenced by an object b then a must appear before b in the library, or reloading will fail.