diff -r 9653bea4aa83 -r bc43f86c9598 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 ***