# HG changeset patch
# User wenzelm
# Date 1737712619 -3600
# Node ID 6d34097215be27e9352d438fd799aaa00d1384dd
# Parent  3d518681bb6c0e0dcb97649f9228e714eb001970
misc tuning for release;

diff -r 3d518681bb6c -r 6d34097215be CONTRIBUTORS
--- a/CONTRIBUTORS	Fri Jan 24 10:48:28 2025 +0100
+++ b/CONTRIBUTORS	Fri Jan 24 10:56:59 2025 +0100
@@ -3,8 +3,8 @@
 listed as an author in one of the source files of this Isabelle distribution.
 
 
-Contributions to this Isabelle version
---------------------------------------
+Contributions to Isabelle2025
+-----------------------------
 
 * October 2024 - January 2025: Lukas Bartl, Universität Augsburg
   Inference of variable instantiations with Metis.
@@ -12,6 +12,10 @@
 * 2024: Fabian Huch, TU München
   Find_Facts search engine: web application based on Apache Solr.
 
+* 2024: Fabian Huch, TU München
+  Build_Manager for distrubuted cluster, with web front-end (supersedes
+  Jenkins).
+
 * April - October 2024: Thomas Lindae and Fabian Huch, TU München
   Improvements to the language server for Isabelle/VSCode.
 
diff -r 3d518681bb6c -r 6d34097215be NEWS
--- a/NEWS	Fri Jan 24 10:48:28 2025 +0100
+++ b/NEWS	Fri Jan 24 10:56:59 2025 +0100
@@ -4,8 +4,8 @@
 (Note: Isabelle/jEdit shows a tree-view of the NEWS file in Sidekick.)
 
 
-New in this Isabelle version
-----------------------------
+New in Isabelle2025 (March 2025)
+--------------------------------
 
 *** General ***
 
@@ -228,18 +228,6 @@
 
 *** HOL ***
 
-* Code generator: command 'code_reserved' now uses parentheses for
-target languages, similar to 'code_printing'.
-
-* Theory HOL.List: overloaded power operator (^^) on type list.
-
-* Theory HOL-Library.Code_Target_Bit_Shifts implemented bit shifts on numeric
-types by target-language operations; this is also used by
-HOL-Library.Code_Target_Numeral.
-
-* Theory HOL-Library.Code_Bit_Shifts_for_Arithmetic rewrites certain
-arithmetic operations on numerals to bit shifts.
-
 * Sledgehammer:
   - Update of bundled provers:
       . E 3.1 -- with patch on Windows/Cygwin for proper interrupts
@@ -257,12 +245,10 @@
     This outputs a suggestion with instantiations of the facts using the
     "of" attribute (e.g. "assms(1)[of x]").
 
-* Theory HOL-Library.Discrete has been renamed
-HOL-Library.Discrete_Functions
-
-  Discrete.log -> floor_log
-  Discrete.sqrt -> floor_sqrt
-  Renamed lemmas accordingly (...log/sqrt... -> ...floor_log/sqrt...)
+* Code generator: command 'code_reserved' now uses parentheses for
+target languages, similar to 'code_printing'.
+
+* Theory HOL.List: overloaded power operator (^^) on type list.
 
 * Theory "HOL.Wellfounded":
   - Removed lemma wellorder.wfP_less. Use wellorder.wfp_on_less instead.
@@ -291,6 +277,30 @@
       wf_on_antimono_stronger
       wfp_on_antimono_stronger
 
+* Theory "HOL.Transcendental": the real-valued versions of ln, log,
+(powr) have been totalised by "ln 0 = x" and "ln (- x) = ln x". Many
+related theorems are now unconditional, with ln_mult_pos and
+ln_divide_pos introduced for legacy purposes.
+
+* Transitional theory "HOL.Divides" moved to "HOL-Library.Divides" and
+supposed to be removed in a future release. Minor INCOMPATIBILITY.
+Import "HOL-Library.Divides" and keep an eye on qualified names with
+prefix "Divides" to ease transition.
+
+* Theory HOL-Library.Code_Target_Bit_Shifts implemented bit shifts on
+numeric types by target-language operations; this is also used by
+HOL-Library.Code_Target_Numeral.
+
+* Theory HOL-Library.Code_Bit_Shifts_for_Arithmetic rewrites certain
+arithmetic operations on numerals to bit shifts.
+
+* Theory HOL-Library.Discrete has been renamed
+HOL-Library.Discrete_Functions to avoid name conflicts:
+
+  Discrete.log -> floor_log
+  Discrete.sqrt -> floor_sqrt
+  Renamed lemmas accordingly (...log/sqrt... -> ...floor_log/sqrt...)
+
 * Theory "HOL-Library.Multiset":
   - Renamed lemmas. Minor INCOMPATIBILITY.
       wfP_less_multiset ~> wfp_less_multiset
@@ -300,17 +310,8 @@
       image_mset_diff_if_inj
       minus_add_mset_if_not_in_lhs[simp]
 
-* Theory "HOL-Library.Suc_Notation" provides compact notation for nested
-Suc terms.
-
-* Transitional theory "HOL.Divides" moved to "HOL-Library.Divides" and
-supposed to be removed in a future release. Minor INCOMPATIBILITY.
-Import "HOL-Library.Divides" and keep an eye on qualified names with prefix
-"Divides" to ease transition.
-
-* The real-valued versions of ln, log, powr have been totalised by "ln 0
-= x" and "ln (- x) = ln x". Many related theorems are now unconditional,
-with ln_mult_pos and ln_divide_pos introduced for legacy purposes.
+* Theory "HOL-Library.Suc_Notation" provides compact notation for
+iterated Suc terms.
 
 
 *** ML ***