Announcing  Proof General  Version 3.5
    A Generic Emacs interface for Interactive Proof Assistants
                 http://proofgeneral.inf.ed.ac.uk

        Contact: David Aspinall <da+pg-feedback@inf.ed.ac.uk>

Proof General is a generic (X)Emacs interface for proof assistants.
It can be instantiated for the proof assistant of your choice, and is
supplied ready-customised for Isabelle, Coq, LEGO, and PhoX, and, 
experimentally, for HOL98, Twelf, and ACL2.

Proof General includes these features, amongst others:

. Script management: proof assistant state reflected in editor
. Toolbar and menus: commands for building and replaying proofs
. Syntax highlighting of proof scripts and prover output; hiding proofs
. Display of real logical symbols, greek letters, etc with X-Symbol
. Activation of prover output for subterm navigation, proof-by-pointing
. Simplified communication: proof assistant verbosity hidden
. Menu for jumping to theorems in a proof script
. Provision to easily run proof assistant on a remote host
. Works on any platform Emacs does, in window system or plain console 

Summary of changes since 3.4:

. FIXME

For details of changes since 3.4, see
http://proofgeneral.inf.ed.ac.uk/fileshow.php?file=ProofGeneral-3.5%2FCHANGES

For the latest user manual, see http://proofgeneral.inf.ed.ac.uk/doc

Proof General needs a recent version of Emacs to run with.  
Proof General 3.5 has been tested with XEmacs 21.1 and 21.4, and 
GNU Emacs 21.2.  Older versions of either XEmacs may work but are not
guaranteed.

Installing Proof General is easy.  Why not give it a try?

 - David Aspinall.
   XXX 2004.