NEWS

--- a/NEWS	Wed Jul 08 16:35:23 2020 +0200
+++ b/NEWS	Thu Jul 09 11:39:16 2020 +0200
@@ -48,6 +48,10 @@
 
 * For the natural numbers, Sup {} = 0.
 
+* Updated the Metis prover underlying the "metis" proof method to
+  version 2.4 (release 20180810). The new version fixes one soundness
+  defect and two incompleteness defects. Very slight INCOMPATIBILITY.
+
 * Library theory "Bit_Operations" with generic bit operations.
 
 * Session HOL-Word: Type word is restricted to bit strings consisting