# 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)"