proof-general 4.4 Generic front-end for proof assistants based on Emacs

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.