diff -r ee3a09458665 -r 3de18e94ac7c 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