NEWS

--- a/NEWS	Wed Sep 17 20:57:11 2025 +0200
+++ b/NEWS	Fri Sep 19 13:11:51 2025 +0200
@@ -196,6 +196,9 @@
 nat are implemented by bit operations on target-language integers. Minor
 INCOMPATIBILITY.
 
+* SMT:
+  - Added Vampire as an SMT solver (experimental).
+
 * Theory "HOL.Fun":
   - Added lemmas.
       antimonotone_on_inf_fun