NEWS
changeset 28605 12d6087ec18c
parent 28604 f36496b73227
child 28606 e5f0f1dd2592
equal deleted inserted replaced
28604:f36496b73227 28605:12d6087ec18c
    95 [code func] has disappeared and only [code] remains.  INCOMPATIBILITY.
    95 [code func] has disappeared and only [code] remains.  INCOMPATIBILITY.
    96 
    96 
    97 * Constant "undefined" replaces "arbitrary" in most occurences.
    97 * Constant "undefined" replaces "arbitrary" in most occurences.
    98 
    98 
    99 * Generic ATP manager for Sledgehammer, based on ML threads instead of
    99 * Generic ATP manager for Sledgehammer, based on ML threads instead of
   100 Posix processes.  Avoids forking of the ML process, can be costly for
   100 Posix processes.  Avoids potentially expensive forking of the ML
   101 long-lived operations due to garbage collection.  New thread
   101 process.  New thread-based implementation also works on non-Unix
   102 based-implementation also works smoothly on non-Unix platforms
   102 platforms (Cygwin).  Provers are no longer hardwired, but defined
   103 (Cygwin).  Provers are no longer hardwired, but defined within the
   103 within the theory via plain ML wrapper functions.
   104 theory via plain ML wrapper functions.
       
   105 
   104 
   106 * Wrapper scripts for remote SystemOnTPTP service allows to use
   105 * Wrapper scripts for remote SystemOnTPTP service allows to use
   107 sledgehammer without local ATP installation (Vampire etc.).  See also
   106 sledgehammer without local ATP installation (Vampire etc.).  See also
   108 ISABELLE_HOME/contrib/SystemOnTPTP and the VAMPIRE_HOME setting
   107 ISABELLE_HOME/contrib/SystemOnTPTP and the VAMPIRE_HOME setting
   109 variable.  Other provers may be included via suitable ML wrappers, see
   108 variable.  Other provers may be included via suitable ML wrappers, see