ProofGeneral
Emacs-based frontend to a variety of theorem provers
ProofGeneral is a powerful frontend for proof assistants based on Emacs. It is generic in that it supports a variety of proof assistants (among others, Isabelle, Lego, and PhoX) and provides for them script management, a simplified interaction model, subterm higlighting and more.
License: GNU GPL.
Tags: automated theorem proving.
Interface: X.
Source language: Emacs Lisp.
Requires GNU Emacs 21 / XEmacs.
Staff
Developer: David Aspinall.
Links
Homepage: http://proofgeneral.inf.ed.ac.uk/devel.
Documentation: http://proofgeneral.inf.ed.ac.uk/develdownload.html.
Mailing lists
Announcements: http://proofgeneral.inf.ed.ac.uk/mailinglist.
Support: http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral.
Development: http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel.
Bugs: da+pg-feedback@inf.ed.ac.uk.
2007–2009 Alexey Beshenov.
Contact: al@cadadr.org.