Organize your proofs!  Home  Features  Download  Documentation  News  Screenshots  Development  About

Documentation and Manuals for Proof General

Proof General is distributed with an FAQ and two manuals:

• 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:

• User manual [pdf] (450k),
• Adapting manual [pdf] (367k)

Both manuals are included in the download (in HTML and Info formats). 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 using the CVS or most recent development version of Proof General, see the documentation available with the development download.

For a growing collection of notes on the usage and development of Proof General, please read and join

• the Proof General Wiki

You can receive occasional announcements about Proof General 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.

Papers about Proof General

Ideas for the future of Proof General

• David Aspinall and Christoph L?th Proof General meets IsaWin. Proc. User Interfaces for Theorem Provers 2003 (UITP'03) September 2003, Rome, Italy. Extended version available as [pdf] (344k).
• David Aspinall. Eclipse Proof General. An Eclipse version of Proof General. Brief outline of plan available as [pdf] (128k).
• David Aspinall. Protocols for Interactive e-Proof. Draft version, see here.
• David Aspinall. Proof General Kit (white paper). Draft version, see here.
• See also the Proof General Kit web page.

A technology overview of Emacs Proof General

• 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.

Related work and older documentation

• 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.
  This paper describes Script Management, also supported by Proof General.

• 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
  This paper describes PG's implementation of Proof by Pointing.