SAL Home OTHERS Artificial Intelligence

Proof General

Proof General is a generic Emacs interface for proof assistants. Proof General works ideally under XEmacs, but can also be used with FSF GNU Emacs. It is supplied ready-customized:

  • LEGO Proof General for LEGO version 1.3.1
  • Coq Proof General for Coq version 6.2
  • Isabelle Proof General for Isabelle version 98-1

Current Version:   2.0

License Type:   ??

Home Site:

Source Code Availability:


Available Binary Packages:

  • Debian Package: No
  • RedHat RPM Package: Yes
  • Other Packages: No

Targeted Platforms:

Linux and others

Software/Hardware Requirements:

Emacs and a proof assistant code mentioned above

Other Links:

Mailing Lists/USENET News Groups:


User Comments:

  • None

See A Screen Shot? (Not Yet)

  SAL Home   |   Other Scientific Fields   |   Artificial Intelligence

Comments? SAL@KachinaTech.COM
Copyright © 1995-2001 by Herng-Jeng Jou
Copyright © 1997-2001 by Kachina Technologies, Inc.
All rights reserved.