Documentation and Resources for Proof General

Proof General has a 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:

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.