NEWS

--- a/NEWS	Tue Feb 14 09:36:35 2023 +0100
+++ b/NEWS	Wed Feb 15 10:56:23 2023 +0100
@@ -228,6 +228,12 @@
 
 * Metis:
   - Made clausifier more robust in the face of nested lambdas.
+    Minor INCOMPATIBILITY.
+
+* Sledgehammer:
+  - Added refutational mode to find likely unprovable conectures. It is
+    enabled by default in addition to the usual proving mode and can be
+    enabled or disabled using the 'refute' option.
 
 
 *** ML ***