Summary of Changes for Proof General 3.1 from 3.0 ================================================= Generic Changes --------------- Fixes for supporting Japan versions of Emacs which have older CL macs with Japanicised documentation. (Japan users, please report any other problems you find, they may be fixable for similar reasons). Minor bug fix for duplicated short output. (set proof-shell-eager-annotation-start-length appropriately) Bug fix with .thy files and X-Symbol mode: subsequently visited theory files would have X-Symbols broken. Bug fix for (non-mule) FSF Emacs 20.5. (Emacs would freeze when starting proof assistant due to character matching problem). Fix for infamous Solaris ^G problem, by setting process-connection-type=nil to force piped communication instead of ptys. (This may have other side effects so please report any you suspect). Coq Changes ----------- LEGO Changes ------------ Isabelle Changes ---------------- Isar Changes ------------ Minor syntax tweaks. Only in the developers' release ------------------------------- * Provisional instantiation of Proof General for Plastic (http://www.dur.ac.uk/CARG/plastic.html) by Paul Callaghan . Internal changes for developers to note --------------------------------------- No changes.