Proof General
Proof General

Organize your proofs!

Documentation and Resources for Proof General

Proof General has an FAQ and two manuals, and places for users:

The Adapting 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:

Both manuals are included in the download (in HTML and Info formats) and available in Info format from inside Proof General. For the CVS or a development version of Proof General, see the development download.

See also the publications page for academic pointers.

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 and further help, these links might be helpful:

You don't need to look at anything about lisp unless you're interested in developing Proof General.
Web pages by David Aspinall. Please report issues on PG trac.
Last modified 22 May 2013.