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 Proof General support for several theorem provers which are not available as packages yet. Phox, Plastic, Twelf.