tuned;
authorwenzelm
Wed Oct 15 21:45:02 2008 +0200 (2008-10-15)
changeset 2860512d6087ec18c
parent 28604 f36496b73227
child 28606 e5f0f1dd2592
tuned;
NEWS
     1.1 --- a/NEWS	Wed Oct 15 21:15:35 2008 +0200
     1.2 +++ b/NEWS	Wed Oct 15 21:45:02 2008 +0200
     1.3 @@ -97,11 +97,10 @@
     1.4  * Constant "undefined" replaces "arbitrary" in most occurences.
     1.5  
     1.6  * Generic ATP manager for Sledgehammer, based on ML threads instead of
     1.7 -Posix processes.  Avoids forking of the ML process, can be costly for
     1.8 -long-lived operations due to garbage collection.  New thread
     1.9 -based-implementation also works smoothly on non-Unix platforms
    1.10 -(Cygwin).  Provers are no longer hardwired, but defined within the
    1.11 -theory via plain ML wrapper functions.
    1.12 +Posix processes.  Avoids potentially expensive forking of the ML
    1.13 +process.  New thread-based implementation also works on non-Unix
    1.14 +platforms (Cygwin).  Provers are no longer hardwired, but defined
    1.15 +within the theory via plain ML wrapper functions.
    1.16  
    1.17  * Wrapper scripts for remote SystemOnTPTP service allows to use
    1.18  sledgehammer without local ATP installation (Vampire etc.).  See also