# HG changeset patch
# User blanchet
# Date 1643702375 -3600
# Node ID f47410c603c61a38fcd2ec7bbd0e0410fc37515e
# Parent  38e24aeeedb8593ccfdb1b4a7809bb32aab2291f
tuned NEWS

diff -r 38e24aeeedb8 -r f47410c603c6 NEWS
--- 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)"