Top > Science > Mathematics > ProofGeneral

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.

Obtaining

Web pagehttp://proofgeneral.inf.ed.ac.uk/devel
Source tarball http://proofgeneral.inf.ed.ac.uk/releases/ProofGeneral-3.5.tar.gz
Source informationhttp://proofgeneral.inf.ed.ac.uk/develdownload.html
Version 3.5 (stable) released on 2004-04-18
Version 3.5.1pre040616 (beta) released on 2004-06-16
Licensed under The GNU General Public License, Version 2 or later.
This is not a GNU package.

Documentation
User manual available in HTML and PDF formats from http://proofgeneral.inf.ed.ac.uk/develdownload.html
Support contacts

Announce Listhttp://proofgeneral.inf.ed.ac.uk/mailinglist
Help List<da+pg-support@inf.ed.ac.uk> http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral
Developer Listhttp://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel <proofgeneral-devel@inf.ed.ac.uk>
Bug List<da+pg-feedback@inf.ed.ac.uk>

Project contacts

Maintainers
Developers
Contributors
  • See the AUTHORS file in the distribution for a complete list

Related information

Source repositorycvs -d :pserver:anon@cvs.inf.ed.ac.uk:/disk/cvs/proofgen login password: anon co ProofGeneral
InterfacesX Window System
Source languagesEmacs Lisp
Use requirementsGNU Emacs 21 or XEmacs

Entry information

License verified byJanet Casey <jcasey@gnu.org> on 2004-06-29
Entry compiled byJanet Casey <jcasey@gnu.org>

Categories


The copyright licensing notice below applies to this text. The software described in this text has its own copyright notice and license, which can usually be found in the distribution itself.

Copyright © 2000, 2001, 2002, 2003, 2004 Free Software Foundation, Inc.

Permission is granted to copy, distribute, and/or modify this document under the terms of the GNU Free Documentation License, Version 1.1 or any later version published by the Free Software Foundation; with no Invariant Sections, with no Front-Cover Texts, and with no Back-Cover Texts. A copy of this license is included in the file COPYING.DOC.

Please report any problems in this page to bug-directory@gnu.org, or find out how you can help fix them.

The FSF provides this directory as a service to the free software community. Please consider donating to the FSF to help support this project.