Documentation and Resources for Proof General
Proof General has a FAQ and two manuals, and places for users:
- Proof General user manual (branch master)
- Adapting Proof General manual (branch master)
- FAQ
- GitHub issues
- Proof General Wiki
- Trac bug tracker (legacy bug tracking system)
- Users mailing list (announcements only)
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:
- User manual (PDF) (505k)
- Adapting manual (PDF) (414k)
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:
- The Emacs user manual
- The Emacs lisp introduction and Emacs lisp reference.
- The Emacs Wiki
You don’t need to look at anything about lisp unless you’re interested in developing Proof General.