# HG changeset patch
# User wenzelm
# Date 1224099902 -7200
# Node ID 12d6087ec18ccfe7f615cd364fcbfdb41fe23969
# Parent  f36496b73227b96c0a66cd8408d59ecb378921ad
tuned;

diff -r f36496b73227 -r 12d6087ec18c NEWS
--- a/NEWS	Wed Oct 15 21:15:35 2008 +0200
+++ b/NEWS	Wed Oct 15 21:45:02 2008 +0200
@@ -97,11 +97,10 @@
 * Constant "undefined" replaces "arbitrary" in most occurences.
 
 * Generic ATP manager for Sledgehammer, based on ML threads instead of
-Posix processes.  Avoids forking of the ML process, can be costly for
-long-lived operations due to garbage collection.  New thread
-based-implementation also works smoothly on non-Unix platforms
-(Cygwin).  Provers are no longer hardwired, but defined within the
-theory via plain ML wrapper functions.
+Posix processes.  Avoids potentially expensive forking of the ML
+process.  New thread-based implementation also works on non-Unix
+platforms (Cygwin).  Provers are no longer hardwired, but defined
+within the theory via plain ML wrapper functions.
 
 * Wrapper scripts for remote SystemOnTPTP service allows to use
 sledgehammer without local ATP installation (Vampire etc.).  See also