Announcing Proof General Version 3.6 A Generic Emacs interface for Interactive Proof Assistants http://proofgeneral.inf.ed.ac.uk 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, and PhoX, and, experimentally, several other systems. 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 . Menus for jumping to theorems/definitions, etc 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 interesting changes since 3.5 (April 2004): . Updates and bug fixes for Coq 8.0 . Extensions for development version of Isabelle, esp. PGIP support Summary of interesting changes since 3.4 (August 2002): . Speedbar and Index Menu. Speedbar provides a handy file/tag tree. . Improved display management. . RPM packages with freedesktop.org integration and compiled files . Keyboard hints and other messages displayed in minibuffer . Improved menus, user options, script colouring and active highlighting . For Coq (8.0): "holes" for editing expressions, extra menus, auto compilation . For Isabelle (2004): browsing/highlighting theorem dependencies . For Isabelle: using LaTeX mode for LaTeX parts of proof documents (via MMM) . New instances of PG: Casl Consistency Checker, Shell Script . Additional sample proofs (some from http://www.cs.kun.nl/~freek/comparison/) . Many other minor improvements and editing features . Many changes for compatibility with latest Emacsen (esp. GNU) and provers . Auxiliary modes bundled: X-Symbol and MMM (Multiple Major Mode) For details of changes since 3.4, see http://proofgeneral.inf.ed.ac.uk/fileshow.php?file=ProofGeneral-3.6%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.6 has been tested with XEmacs 21.4.15, and GNU Emacs 21.3.1. Other recent versions of either Emacs may work but are not guaranteed. - David Aspinall. September 2004.