# HG changeset patch
# User wenzelm
# Date 1739116615 -3600
# Node ID 56ced64166d22385fd0d5ec49a21f7b18d13d666
# Parent  a6a3ba4f715732a3163c2b8130c163c159bf6246
tuned NEWS for release;

diff -r a6a3ba4f7157 -r 56ced64166d2 NEWS
--- a/NEWS	Sun Feb 09 16:24:20 2025 +0100
+++ b/NEWS	Sun Feb 09 16:56:55 2025 +0100
@@ -190,10 +190,11 @@
 
 * Update to jEdit 5.7.0, the latest release.
 
-* Update to FlatLaf 3.5.4, the latest release. Starting with version 3.x
-there is native library support for non-portable GUI operations. The
-Isabelle/Scala GUI setup disables that by default, for cross-platform
-uniformity (arm64-linux lacks a native library).
+* Update GUI look-and-feel to FlatLaf 3.5.4, the latest release.
+Starting with version 3.x there is native library support for
+non-portable GUI operations. The Isabelle/Scala GUI setup disables that
+by default, for cross-platform uniformity (arm64-linux lacks a native
+library).
 
 * Thanks to the update of FlatLaf, Linux with Wayland window manager
 (e.g. standard Ubuntu) now renders submenus like "File / Recent Files"
@@ -263,11 +264,10 @@
   - Use pretty-printing to format suggested one-line proofs.
   - Added option "cache_dir" to cache the result of external provers.
 
-* Metis:
-  - Added inference of variable instantiations, which can be activated
-    using the configuration option "metis_instantiate" (default: false).
-    This outputs a suggestion with instantiations of the facts using the
-    "of" attribute (e.g. "assms(1)[of x]").
+* Metis: Added inference of variable instantiations, which can be
+activated using the configuration option "metis_instantiate" (default:
+false). This outputs a suggestion with instantiations of the facts using
+the "of" attribute (e.g. "assms(1)[of x]").
 
 * Code generator: command 'code_reserved' now uses parentheses for
 target languages, similar to 'code_printing'.
@@ -277,6 +277,9 @@
 e.g. extend the order solver to deal with numerals. In Isabelle/HOL,
 hooks can be added with HOL_Base_Order_Tac.declare_insert_prems_hook.
 
+* Theory "HOL.Nat": thm "of_nat_diff" is now declared as [simp]. Minor
+INCOMPATIBILITY.
+
 * Theory "HOL.Wellfounded":
   - Removed lemma wellorder.wfP_less. Use wellorder.wfp_on_less instead.
     Minor INCOMPATIBILITY.
@@ -343,8 +346,6 @@
 * Theory "HOL-Library.Suc_Notation" provides compact notation for
 iterated Suc terms.
 
-* Theory "HOL.Nat": of_nat_diff is now a simprule, minor INCOMPATIBILITY.
-
 * Theory "HOL-Library.Adhoc_Overloading" has been moved to Pure. Minor
 INCOMPATIBILITY: need to adjust theory imports.