--- a/NEWS Mon Jan 21 22:29:41 2019 +0100
+++ b/NEWS Mon Jan 21 22:46:25 2019 +0100
@@ -110,8 +110,11 @@
are now uniformly called f_cong_simp, in accordance with congruence
rules produced for mappers by the datatype package. INCOMPATIBILITY.
-* Sledgehammer: The URL for SystemOnTPTP, which is used by remote
-provers, has been updated.
+* Sledgehammer:
+ - The URL for SystemOnTPTP, which is used by remote provers, has
+ been updated.
+ - The machine-learning-based filter MaSh has been optimized to take
+ less time (in most cases).
* SMT: reconstruction is now possible using the SMT solver veriT.