1.1 --- a/NEWS	Wed Oct 15 21:06:15 2008 +0200
     1.2 +++ b/NEWS	Wed Oct 15 21:15:35 2008 +0200
     1.3 @@ -91,15 +91,23 @@
     1.4  
     1.5  *** HOL ***
     1.6  
     1.7 -* Unified theorem tables for both code code generators.  Thus [code func]
     1.8 -has disappeared and only [code] remains.  INCOMPATIBILITY.
     1.9 -
    1.10 -* "undefined" replaces "arbitrary" in most occurences.
    1.11 -
    1.12 -* Wrapper script for remote SystemOnTPTP service allows to use
    1.13 +* Unified theorem tables for both code code generators.  Thus
    1.14 +[code func] has disappeared and only [code] remains.  INCOMPATIBILITY.
    1.15 +
    1.16 +* Constant "undefined" replaces "arbitrary" in most occurences.
    1.17 +
    1.18 +* Generic ATP manager for Sledgehammer, based on ML threads instead of
    1.19 +Posix processes.  Avoids forking of the ML process, can be costly for
    1.20 +long-lived operations due to garbage collection.  New thread
    1.21 +based-implementation also works smoothly on non-Unix platforms
    1.22 +(Cygwin).  Provers are no longer hardwired, but defined within the
    1.23 +theory via plain ML wrapper functions.
    1.24 +
    1.25 +* Wrapper scripts for remote SystemOnTPTP service allows to use
    1.26  sledgehammer without local ATP installation (Vampire etc.).  See also
    1.27  ISABELLE_HOME/contrib/SystemOnTPTP and the VAMPIRE_HOME setting
    1.28 -variable.
    1.29 +variable.  Other provers may be included via suitable ML wrappers, see
    1.30 +also src/HOL/ATP_Linkup.thy.
    1.31  
    1.32  * Normalization by evaluation now allows non-leftlinear equations.
    1.33  Declare with attribute [code nbe].