<freeze-command> ::= (freeze | freeze-current) <file> <thaw-command> ::= thaw <file>
freeze case1 thaw case1
The freeze-current command does the same, except that it only saves the state of the current proof context. This command is faster and uses less disk space than the freeze command. It is useful primarily for trying different strategies for proving the current conjecture.
The thaw command restores the state of LP from that saved previously using the freeze command in the file named <file>.lpfrz (unless <file> contains a period, in which case LP does not supply the suffix .lpfrz) on the current LP search path. The thaw command will not thaw files that were frozen using an out-of-date version of LP.
These commands are useful for checkpointing attempted proofs. They are also useful for saving and restoring completed or partially-completed systems.