--- 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)
------------------------------------