Summary of Changes for Proof General 2.1 ---------------------------------------- * Supports Coq 6.3 * Supports Isabelle 99. No guarantees for Isabelle 98. * Two new provisional instantiations of Proof General, for: ** Isabelle/Isar (new proof language for Isabelle) by Markus Wenzel ** Plastic (http://www.dur.ac.uk/CARG/plastic.html) by Paul Callaghan . * Documentation improvements. Information added for Coq mode. * In proof-site.el, the environment variable PROOFGENERAL_ASSISTANTS is examined for the default value of proof-assistants. No editing of proof-site.el should be needed now. * Support for x-symbol package to beautify input and output with special fonts. Patches for Isabelle provided by David von Oheimb. (currently incomplete) * Improvements to Coq mode: better recognition of Coq syntax, support for proof-shell-restart-cmd. * Toolbar can now be switched on and off via menu. * Bug fixes: - Long-lines with funny characters causing ^G's in Solaris. - Templates in Isabelle theory file mode. - Fix for case-insensitive matching. Added proof-case-fold-search configuration variable to allow for proof script languages with case-insensitive syntax. - Process killing made robust. - Regular expression fixes causing "nil extent" errors.