# HG changeset patch
# User wenzelm
# Date 1224098135 -7200
# Node ID f36496b73227b96c0a66cd8408d59ecb378921ad
# Parent  b40800eef8a7b65660a449c0a11d6563d160c1c1
generic ATP manager based on threads (by Fabian Immler);

diff -r b40800eef8a7 -r f36496b73227 CONTRIBUTORS
--- a/CONTRIBUTORS	Wed Oct 15 21:06:15 2008 +0200
+++ b/CONTRIBUTORS	Wed Oct 15 21:15:35 2008 +0200
@@ -7,6 +7,11 @@
 Contributions to this Isabelle version
 --------------------------------------
 
+* October 2008: Fabian Immler, TUM
+  ATP manager for Sledgehammer, based on ML threads instead of Posix
+  processes.  Additional ATP wrappers, including remote SystemOnTPTP
+  services.
+
 * August 2008: Fabian Immler, TUM
   Vampire wrapper script for remote SystemOnTPTP service.
 
diff -r b40800eef8a7 -r f36496b73227 NEWS
--- a/NEWS	Wed Oct 15 21:06:15 2008 +0200
+++ b/NEWS	Wed Oct 15 21:15:35 2008 +0200
@@ -91,15 +91,23 @@
 
 *** HOL ***
 
-* Unified theorem tables for both code code generators.  Thus [code func]
-has disappeared and only [code] remains.  INCOMPATIBILITY.
-
-* "undefined" replaces "arbitrary" in most occurences.
-
-* Wrapper script for remote SystemOnTPTP service allows to use
+* Unified theorem tables for both code code generators.  Thus
+[code func] has disappeared and only [code] remains.  INCOMPATIBILITY.
+
+* 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.
+
+* Wrapper scripts for remote SystemOnTPTP service allows to use
 sledgehammer without local ATP installation (Vampire etc.).  See also
 ISABELLE_HOME/contrib/SystemOnTPTP and the VAMPIRE_HOME setting
-variable.
+variable.  Other provers may be included via suitable ML wrappers, see
+also src/HOL/ATP_Linkup.thy.
 
 * Normalization by evaluation now allows non-leftlinear equations.
 Declare with attribute [code nbe].