NEWS
changeset 28606 e5f0f1dd2592
parent 28605 12d6087ec18c
child 28629 c5a915b45390
equal deleted inserted replaced
28605:12d6087ec18c 28606:e5f0f1dd2592
    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 potentially expensive forking of the ML
   100 Posix processes.  Avoids potentially expensive forking of the ML
   101 process.  New thread-based implementation also works on non-Unix
   101 process.  New thread-based implementation also works on non-Unix
   102 platforms (Cygwin).  Provers are no longer hardwired, but defined
   102 platforms (Cygwin).  Provers are no longer hardwired, but defined
   103 within the theory via plain ML wrapper functions.
   103 within the theory via plain ML wrapper functions.  Basic Sledgehammer
       
   104 commands are covered in the isar-ref manual
   104 
   105 
   105 * Wrapper scripts for remote SystemOnTPTP service allows to use
   106 * Wrapper scripts for remote SystemOnTPTP service allows to use
   106 sledgehammer without local ATP installation (Vampire etc.).  See also
   107 sledgehammer without local ATP installation (Vampire etc.).  See also
   107 ISABELLE_HOME/contrib/SystemOnTPTP and the VAMPIRE_HOME setting
   108 ISABELLE_HOME/contrib/SystemOnTPTP and the VAMPIRE_HOME setting
   108 variable.  Other provers may be included via suitable ML wrappers, see
   109 variable.  Other provers may be included via suitable ML wrappers, see