Storing Results

The load and dump commands let one save results between sessions.

dump objects

 

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.

load place from filename

  This is the command used to read in a file produced by dump. The decoded library entries are added to the library starting at location place. If an object in the dumped file has the same name as an object already in the library, the object in the file is ignored. When the load is finished a message is displayed giving the number of objects loaded and the number of duplicates discarded. The name of the loaded file is displayed in the header of the library window.

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.