Manual

Full documentation for Proof General is included in the When running Proof General the manual is available from the "Proof General" menu. It should also appear in the system info pages.

For convenience, the manual is available in HTML
For printing you can download the .

Warning: the manual above is taken from the current pre-release and may be updated from the documentation included in the last stable release.

You can discuss Proof General with other users and receive announcements by joining our mailing lists.

References

Proof General supports Script Management as documented in:

• Yves Bertot and Laurent Théry. A generic approach to building user interfaces for theorem provers. Journal of Symbolic Computation, 25(7), pp. 161-194, February 1998.

It has support for Proof by Pointing, as documented in:

• Yves Bertot, Thomas Kleymann-Schreiber and Dilip Sequeira. Implementing Proof by Pointing without a Structure Editor. LFCS Technical Report ECS-LFCS-97-368. Also published as Rapport de recherche de l'INRIA Sophia Antipolis RR-3286