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.
|Tags||Scientific/Engineering Mathematics Text Editors Emacs|
|Operating Systems||Windows Mac OS X POSIX Linux|
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.
Release Notes: This resolves some compatibility issues for Isabelle and adds some improvements for Coq.
No changes have been submitted for this release.