1.1 --- a/CONTRIBUTORS	Wed Oct 15 21:06:15 2008 +0200
     1.2 +++ b/CONTRIBUTORS	Wed Oct 15 21:15:35 2008 +0200
     1.3 @@ -7,6 +7,11 @@
     1.4  Contributions to this Isabelle version
     1.5  --------------------------------------
     1.6  
     1.7 +* October 2008: Fabian Immler, TUM
     1.8 +  ATP manager for Sledgehammer, based on ML threads instead of Posix
     1.9 +  processes.  Additional ATP wrappers, including remote SystemOnTPTP
    1.10 +  services.
    1.11 +
    1.12  * August 2008: Fabian Immler, TUM
    1.13    Vampire wrapper script for remote SystemOnTPTP service.
    1.14  

     2.1 --- a/NEWS	Wed Oct 15 21:06:15 2008 +0200
     2.2 +++ b/NEWS	Wed Oct 15 21:15:35 2008 +0200
     2.3 @@ -91,15 +91,23 @@
     2.4  
     2.5  *** HOL ***
     2.6  
     2.7 -* Unified theorem tables for both code code generators.  Thus [code func]
     2.8 -has disappeared and only [code] remains.  INCOMPATIBILITY.
     2.9 -
    2.10 -* "undefined" replaces "arbitrary" in most occurences.
    2.11 -
    2.12 -* Wrapper script for remote SystemOnTPTP service allows to use
    2.13 +* Unified theorem tables for both code code generators.  Thus
    2.14 +[code func] has disappeared and only [code] remains.  INCOMPATIBILITY.
    2.15 +
    2.16 +* Constant "undefined" replaces "arbitrary" in most occurences.
    2.17 +
    2.18 +* Generic ATP manager for Sledgehammer, based on ML threads instead of
    2.19 +Posix processes.  Avoids forking of the ML process, can be costly for
    2.20 +long-lived operations due to garbage collection.  New thread
    2.21 +based-implementation also works smoothly on non-Unix platforms
    2.22 +(Cygwin).  Provers are no longer hardwired, but defined within the
    2.23 +theory via plain ML wrapper functions.
    2.24 +
    2.25 +* Wrapper scripts for remote SystemOnTPTP service allows to use
    2.26  sledgehammer without local ATP installation (Vampire etc.).  See also
    2.27  ISABELLE_HOME/contrib/SystemOnTPTP and the VAMPIRE_HOME setting
    2.28 -variable.
    2.29 +variable.  Other provers may be included via suitable ML wrappers, see
    2.30 +also src/HOL/ATP_Linkup.thy.
    2.31  
    2.32  * Normalization by evaluation now allows non-leftlinear equations.
    2.33  Declare with attribute [code nbe].