When a theory is dumped to a file , proofs are stored in a compressed format . This format retains only the main goal, the text of tactics in tactic rules, and the text of primitive rules not buried inside tactic rules. All other sequents, and all subproofs associated with tactic rules, are discarded. Thus the dumped representation contains essentially just the text that a user would type to reconstruct the proof .
This format contains just enough information to regenerate the full proof data-structure. When a theory is loaded, the loaded proofs are retained in their compressed format. When a proof is needed, as when it is to be viewed, checked, or extracted from, then the system will reconstruct the usual proof tree.
The reconstruction can be time consuming since all the tactics used to construct the proof must be re-executed. Also, if the tactics that were used to construct the proofs have since been modified, the reconstruction may fail.
When a theorem object is extracted from, the extraction is stored with the theorem in the library. When a theorem object is dumped to a file, if it has an extraction, then the extraction is also dumped. This feature can sometimes reduce the need for proof expansion.
The proof-script of a theorem is updated whenever a complete proof of the theorem is built. Note however that it is not updated if expansion of a previously complete theorem results in an incomplete theorem. This is to give the user a chance to fix the proof script. The proof-script of a theorem is also updated when a theorem is dumped to a file, and when the proof is compressed.