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. It works with either XEmacs or GNU Emacs. . This package provides the HTML documentation for Proof General. It was created from the same sources as the info documentation which is included in the proofgeneral package.