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