diff -r 56ef403eab15 -r b452242dce36 NEWS
--- a/NEWS	Wed Oct 14 22:30:18 2020 +0200
+++ b/NEWS	Thu Oct 15 13:24:16 2020 +0200
@@ -70,6 +70,11 @@
 
 *** HOL ***
 
+* An updated version of the veriT solver is now included as Isabelle
+component. It can be used in the "smt" proof method via "smt (verit)" or
+via "declare [[smt_solver = verit]]" in the context; see also session
+HOL-Word-SMT_Examples.
+
 * Nitpick/Kodkod may be invoked directly within the running
 Isabelle/Scala session (instead of an external Java process): this
 improves reactivity and saves resources. This experimental feature is
@@ -158,9 +163,6 @@
 are in working order again, as opposed to outputting "GaveUp" on nearly
 all problems.
 
-* SMT reconstruction: It is now possible to reconstruct proofs from the
-SMT solver veriT by calling "smt (verit)".
-
 
 *** FOL ***