This version of Proof General has been tested with these Emacs versions on Linux: Emacs 21.4.1 -- recommended XEmacs 21.4.XX -- stable, but not recently tested XEmacs 21.5 (beta28) -- tested, has patches for several XEmacs bugs and prover versions: Coq 8.1 Isabelle2005 Isabelle2007 For more possibilities, please check and contribute here: http://proofgeneral.inf.ed.ac.uk/wiki/Main/PGEmacsVer37Final