NEWS
changeset 78149 d3122089b67c
parent 78143 7ea4f986e41a
child 78150 2963ea647c2a
--- a/NEWS	Wed Jun 07 17:09:17 2023 +0200
+++ b/NEWS	Wed Jun 14 15:47:27 2023 +0200
@@ -64,11 +64,11 @@
 
 * Sledgehammer:
   - Added an inconsistency check mode to find likely unprovable
-    conjectures. It is enabled by default in addition to the usual
-    proving mode and can be controlled using the 'falsify' option.
+    conjectures. It is disabled by default and can be controlled using
+    the 'falsify' option.
   - Added an abduction mode to find likely missing hypotheses to
-    conjectures. It currently works only with the E prover. It is
-    enabled by default and can be controlled using the 'abduce' option.
+    conjectures. It works only with the E prover. It is disabled by
+    default and can be controlled using the 'abduce' option.
 
 * Metis:
   - Made clausifier more robust in the face of nested lambdas.