--- 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