To: coq-club@pauillac.inria.fr, isabelle-users@cl.cam.ac.uk, lego-club@dcs.ed.ac.uk, uitp@dcs.gla.ac.uk, bra-types@cs.chalmers.se, info-hol@leopard.cs.byu.edu, pvs@csl.sri.com, qed@mcs.anl.gov, theorem-provers@ai.mit.edu, types@cis.upenn.edu, formal-methods@cs.uidaho.edu, reliable_computing@interval.usl.edu, prog-lang@diku.dk Also newsgroups: comp.lang.ml comp.lang.functional gnu.emacs.sources comp.emacs.xemacs comp.os.linux.announce freshmeat.net tag for comp.lang.ml, comp.lang.functional: [Posted here because ML and functional languages generally are traditional for implementing interactive theorem provers. Implementors of such systems may be interested in Proof General. Apologies for multiple copies] Subject: Proof General --- Version 3.2 release Announcing Proof General Version 3.2 A Generic Emacs interface for Interactive Proof Assistants http://www.proofgeneral.org contact: David Aspinall 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, HOL, and AF2. 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 . Display of real logical symbols, greek letters, etc . 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.1: . New provers: AF2 (full support) Twelf, ACL2 (experimental support) . Each proof assistant now has its own menu with specific functions . Documentation is now split into user manual and "adapting" manual . Improvements in window management . New commands, including parsing of error messages . Efficiency improvements . Several bug fixes . Internal improvements: more flexible parsing and easier configuration . For details, see http://www.proofgeneral.org/ProofGeneral-3.2/CHANGES The user manual contains full details, and is available on-line at: http://www.proofgeneral.org/index.html?page=doc Proof General needs a recent version of Emacs to run with, and it much prefers XEmacs to FSF GNU Emacs. Proof General 3.2 has been tested with XEmacs 21.1 and Emacs 20.7. (It may work back to XEmacs 20.4 and Emacs 20.2, though). Installing Proof General is easy. Why not give it a try? - David Aspinall October 2000.