Proof general is a major mode to turn emacs into an interactive proof assistant to write formal mathematical proofs using a variety of theorem provers.

this package provides the proof general user manual in info, html and pdf form.