NEWS

--- a/NEWS	Wed Oct 22 21:56:50 2025 +0200
+++ b/NEWS	Thu Oct 23 14:49:21 2025 +0200
@@ -211,6 +211,9 @@
   - Splitted option "smt_debug_files" into "smt_problem_dest_dir" and
     "smt_proof_dest_dir". Minor INCOMPATIBILITY.
 
+* Sledgehammer:
+  - Don't suggest proofs by `smt (z3)` anymore.
+
 * Theory "HOL.Fun":
   - Added lemmas.
       antimonotone_on_inf_fun