# HG changeset patch
# User blanchet
# Date 1643641763 -3600
# Node ID 094ba0948403742258f6e5b785d2fc32796d3ee3
# Parent  e5750bcb8c412c7f5a4038c35128e46850378f86
updated NEWS

diff -r e5750bcb8c41 -r 094ba0948403 NEWS
--- a/NEWS	Mon Jan 31 16:09:23 2022 +0100
+++ b/NEWS	Mon Jan 31 16:09:23 2022 +0100
@@ -35,6 +35,10 @@
   - Redefined less_multiset to be based on multp. INCOMPATIBILITY.
 
 * Sledgehammer:
+  - Redesigned multithreading to provide more fine grained prover scheduled.
+    The binary option 'slice' has been replaced by a numeric value 'slices'
+    indicating the number of desired slices. Stronger provers can now be run by
+    more than one thread simultaneously. INCOMPATIBILITY.
   - Introduced sledgehammer_outcome data type and changed return type of ML
     function Sledgehammer.run_sledgehammer from "bool * (string * string list)"
     to "bool * (sledgehammer_outcome * string)". The former value can be
@@ -46,6 +50,7 @@
   - Replaced option "sledgehammer_atp_dest_dir" by
     "sledgehammer_atp_problem_dest_dir", for problem files, and
     "sledgehammer_atp_proof_dest_dir", for proof files. Minor INCOMPATIBILITY.
+  - Removed support for experimental prover 'z3_tptp'.
 
 * Mirabelle:
   - Replaced sledgehammer option "keep" by