--- a/NEWS Sat Oct 14 20:24:39 2023 +0200
+++ b/NEWS Sat Oct 14 20:48:12 2023 +0200
@@ -7,11 +7,13 @@
New in this Isabelle version
----------------------------
-*** System ***
-
-* Isabelle/Scala and derived Scala tools now use the syntax of Scala
-3.3, instead of 3.1. This is the "-old-syntax" variant (Java-like) as
-before, not "-new-syntax" (Python-like). Minor INCOMPATIBILITY.
+*** 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.
*** ML ***
@@ -40,13 +42,11 @@
specific. Subtle INCOMPATIBILITY in the semantics of ML evaluation.
-*** 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.
+*** System ***
+
+* Isabelle/Scala and derived Scala tools now use the syntax of Scala
+3.3, instead of 3.1. This is the "-old-syntax" variant (Java-like) as
+before, not "-new-syntax" (Python-like). Minor INCOMPATIBILITY.