Manuals for Proof General

There is a short FAQ and two manuals for Proof General:

• the FAQ (please send any contributions)
• the Proof General user manual
• the Adapting Proof General manual

The second manual gives instructions on how to adapt Proof General to new proof systems, it's not needed for ordinary use. For printing you can download:

• and , or
• ,

The PostScript files are recommended over the PDF. Both manuals (HTML and Info formats) are included in the download. When running Proof General the manual is available from the "Proof General" menu. It should also appear in the system Info pages. If you're considering developing Proof General, please check that you are using the documentation for the most recent development version of Proof General, available with the development download.

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

Manuals for Emacs

If you're new to Emacs, it's recommended to try the Emacs tutorial, available inside Emacs by pressing C-h t (which means ctrl-with-h followed by t). There are many other C-h commands, and the Help menu inside Emacs gives access to more help facilities.

For on-line reading, these links might be helpful:

• The Emacs user manual
• The Emacs lisp introduction and Emacs lisp reference.

The corresponding manuals for XEmacs are available here (xemacs.org).

References

Ideas for the future of Proof General are given here:

• David Aspinall. Protocols for Interactive e-Proof. Draft version, see here.
• David Aspinall. Proof General Kit (white paper). Draft version, see here.

A technology overview of Proof General is given here:

• David Aspinall. Proof General: A Generic Tool for Proof Development. Tools and Algorithms for the Construction and Analysis of Systems, Proc TACAS 2000, LNCS 1785.
  Here are some slides used for this talk and some other presentations of Proof General.

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