--- a/NEWS Fri Jan 25 14:54:49 2008 +0100
+++ b/NEWS Fri Jan 25 22:03:29 2008 +0100
@@ -16,11 +16,12 @@
*** Pure ***
-* Instantiation target allows for simultaneous specification of class instance
-operations together with an instantiation proof. Type check phase allows to
-refer to class operations uniformly. See HOL/Complex/Complex.thy for an Isar
-example and HOL/Library/Eval.thy for an ML example.
-Superseedes some immature attempts.
+* Instantiation target allows for simultaneous specification of class
+instance operations together with an instantiation proof.
+Type-checking phase allows to refer to class operations uniformly.
+See HOL/Complex/Complex.thy for an Isar example and
+HOL/Library/Eval.thy for an ML example. Supersedes previous
+experimental versions.
*** HOL ***
@@ -85,6 +86,9 @@
*** System ***
+* Default settings: PROOFGENERAL_OPTIONS no longer impose xemacs here
+--- in accordance with Proof General 3.7, which prefers GNU emacs.
+
* Multithreading.max_threads := 0 refers to the number of actual CPU
cores of the underlying machine, which is a good starting point for
optimal performance tuning. The corresponding usedir option -M allows