To: coq-club@pauillac.inria.fr, isabelle-users@cl.cam.ac.uk, lego-club@dcs.ed.ac.uk
Subject: Proof General --- Version 2.0 release


Proof General is a generic Emacs interface for proof assistants. It is
supplied ready-customised for LEGO, Coq, and Isabelle.  Details are on
the web at:

  http://www.dcs.ed.ac.uk/home/proofgen/

The interface includes these features:

 . script management: files and regions of files processed by prover
   have a blue background and are read-only.  Works across multiple
   files for LEGO and Isabelle.
 . a toolbar for building and replaying proofs
 . syntax highlighting of proof scripts and prover output
 . menu for jumping to theorems in a proof script
 . provision to run proof assistant on a remote host

and several more besides.  The code is designed to be adaptable to
other proof assistants, by writing a little bit of Emacs Lisp.

This is the first official release of Proof General.  It should be
stable enough for LEGO, Coq, and Isabelle users to use happily.

We'd like to encourage users to try it out and let us know what they
think.  We have put a lot of work into making Proof General robust and
easy to install.  It runs ideally with XEmacs, but also works with FSF
Emacs.  We have tested on XEmacs 20.4 and Emacs 20.2,20.3 (but it
probably works with earlier versions).


 -- David Aspinall & Thomas Kleymann
    (Please contact via  proofgen@dcs.ed.ac.uk)