Reverting to a Previous Proof Level (rpl)

The results of an automatic/btool proof session may be removed using the Revert to a Previous Level (rpl) option in the Provers Environment, when a proof level preceding the current one may be substituted. The option is available only when at least one autoproof/btoolproof has currently been performed. Remake will attempt to rebuild the proof level.

A full on-line help listing is available in the Contents Page Also available in the form of a complete Index. Blogo