HOL/ex/Chinese.thy;
authorwenzelm
Tue, 20 Sep 2005 14:20:58 +0200
changeset 17519 9c10585a238c
parent 17518 87b49367ee9b
child 17520 8581c151adea
HOL/ex/Chinese.thy; PROOFGENERAL_OPTIONS: no longer prefer xemacs;
NEWS
--- a/NEWS	Tue Sep 20 14:17:31 2005 +0200
+++ b/NEWS	Tue Sep 20 14:20:58 2005 +0200
@@ -46,12 +46,18 @@
 * Communication with Proof General is now 8bit clean, which means that
 Unicode text in UTF-8 encoding may be used within theory texts (both
 formal and informal parts).  Cf. option -U of the Isabelle Proof
-General interface; HOL/ex/Hebrew.thy provides a simple example.
+General interface; see HOL/ex/Hebrew.thy and HOL/ex/Chinese.thy for
+some simple examples.
 
 * Improved efficiency of the Simplifier and, to a lesser degree, the
 Classical Reasoner.  Typical big applications run around 2 times
 faster.
 
+* ProofGeneral interface: the default settings no longer prefer xemacs
+over GNU emacs.  Users typically need to experiment with various
+variations on PROOFGENERAL_OPTIONS="... -p emacs" to find the most
+stable Emacs version on their platform.
+
 
 *** Document preparation ***