# HG changeset patch
# User wenzelm
# Date 1697309292 -7200
# Node ID d495e71707d454561a4076c1f1456b4a06005002
# Parent  3b424f9cd5ebf342c78faf0f4fce72abee0e3db3
tuned structure;

diff -r 3b424f9cd5eb -r d495e71707d4 NEWS
--- 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.