A Parameterized Proof Manager
Proof management is an important issue for interactive theorem
provers. We describe a simple proof manager that derives a large measure
of its power from being parameterized by structures that separately
manage 1) proof-specific information and 2) the relationships between
proofs. Examples of its use include mixed forward and backward proof,
automatic proof logging and replay, support for documenting a proof
either before, during, or after the proof effort, and the management of
proof dependencies.
paper