# HG changeset patch
# User desharna
# Date 1696238903 -7200
# Node ID 183a28459663e573d55be14299fcbf196e74d234
# Parent  45867a453a3f1d862f388692b25cd09f2ce58b70
NEWS

diff -r 45867a453a3f -r 183a28459663 NEWS
--- a/NEWS	Mon Oct 02 11:22:53 2023 +0200
+++ b/NEWS	Mon Oct 02 11:28:23 2023 +0200
@@ -34,6 +34,15 @@
 as last resort declare [[ML_catch_all]] within the theory context.
 
 
+*** HOL ***
+
+* Mirabelle:
+  - Removed proof reconstruction from "sledgehammer" action; the related option
+  "proof_method" was removed. Proof reconstruction is supported directly
+  by Sledgehammer and should be used instead. For more information, see
+  Sledgehammer's documentation relating to "preplay_timeout". INCOMPATIBILITY.
+
+
 
 New in Isabelle2023 (September 2023)
 ------------------------------------