Projects / Proof General

Proof General

Proof General is a generic Emacs interface for proof assistants, suitable for use by pacifists and Emacs militants alike. It is supplied ready-customized for LEGO, Coq, and Isabelle. You can adapt Proof General to other proof assistants if you know a little bit of Emacs Lisp.

Operating Systems

Recent releases

  •  28 Apr 2011 09:28

    Release Notes: Upgrades were made for compatibility with newer proof assistants. Various new features were added. Compatibility with XEmacs was dropped and X-Symbol was replaced with a new mode called Unicode Tokens written specially for Proof General.

    •  24 Jan 2010 08:19

      Release Notes: This resolves some compatibility issues for Isabelle and adds some improvements for Coq.

      •  16 Dec 1998 19:59

        No changes have been submitted for this release.


        Project Spotlight


        A Fluent OpenStack client API for Java.


        Project Spotlight

        TurnKey TWiki Appliance

        A TWiki appliance that is easy to use and lightweight.