--- a/NEWS Mon Jan 31 16:09:23 2022 +0100
+++ b/NEWS Tue Feb 01 08:59:35 2022 +0100
@@ -35,10 +35,10 @@
- Redefined less_multiset to be based on multp. INCOMPATIBILITY.
* Sledgehammer:
- - Redesigned multithreading to provide more fine grained prover scheduled.
+ - Redesigned multithreading to provide more fine grained prover schedules.
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. The new parameter 'max_proofs' controls
+ more than one thread simultaneously. The new option 'max_proofs' controls
the number of proofs shown. INCOMPATIBILITY.
- Introduced sledgehammer_outcome data type and changed return type of ML
function Sledgehammer.run_sledgehammer from "bool * (string * string list)"