Before downloading Proof General, please
register.
It only takes a moment.
The information collected will be used to help a case for
support for Proof General, and nothing else.
It is likely that development of Proof General will
finish very soon unless we can find new
resources.
If you have already registered you do not need to do so again.
You may like to consider joining the Proof General mailing list.
Developers and beta-testers may like to download a development release of Proof General.
If you are using an older version of a proof assistant, you may wish to check the previous releases of Proof General.
This version of Proof General has been tested
with XEmacs 20.4, XEmacs 21 and FSF Emacs 20.3.
It supports Coq version 6.3, LEGO version 1.3.1 and
some pre-release versions of Isabelle version 99.
Check the file
for a summary of changes since version 2.0.
Proof General is available in two formats:
Both the tarball and the RPM package include the generic elisp
code,
code for LEGO, Coq, and Isabelle, installation instructions
and documentation.
To use Proof General, simply unpack the sources with
tar -xpzf ProofGeneral-2.1.tar.gz
(use gunzip first in place of -z if you don't have GNU tar),
and then add this one line to your .emacs file:
(load-file "directory/generic/proof-site.el")
Where directory is the directory in which you unpacked
the sources.
If you use the RPM package, directory is
/usr/share/emacs/ProofGeneral
Further customization is possible via the Customize menus in
Emacs.
See the
file in the distribution for more details.
Please send us any problems, suggestions, or patches.