--- 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
--- a/etc/settings Fri Jan 25 14:54:49 2008 +0100
+++ b/etc/settings Fri Jan 25 22:03:29 2008 +0100
@@ -208,10 +208,7 @@
"$ISABELLE_INTERFACE")
PROOFGENERAL_OPTIONS=""
-#PROOFGENERAL_OPTIONS="-m no_brackets -m no_type_brackets -x true -p xemacs"
-
-type -path xemacs >/dev/null || \
- PROOFGENERAL_OPTIONS="-p emacs $PROOFGENERAL_OPTIONS"
+#PROOFGENERAL_OPTIONS="-m no_brackets -m no_type_brackets -x true -p emacs22"
# Automatic setup of remote fonts
#XSYMBOL_INSTALLFONTS="xset fp+ tcp/isafonts.informatik.tu-muenchen.de:7200"