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

RSS Recent releases

  •  28 Apr 2011 12:05

    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 09:31

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

      •  30 Jan 2001 06:13

        No changes have been submitted for this release.


        Project Spotlight


        The NTRU public-key cryptosystem.


        Project Spotlight


        A lightweight, RESTful server for medical imaging.