# HG changeset patch
# User wenzelm
# Date 1735818579 -3600
# Node ID 0b088316b8a36c9dddb0aa2faa7123021a6a1270
# Parent  fcc7a78b7220372f5bffa9ed99f911ccbaa9949d
misc tuning and updates for release;

diff -r fcc7a78b7220 -r 0b088316b8a3 CONTRIBUTORS
--- a/CONTRIBUTORS	Thu Jan 02 12:14:51 2025 +0100
+++ b/CONTRIBUTORS	Thu Jan 02 12:49:39 2025 +0100
@@ -7,7 +7,7 @@
 --------------------------------------
 
 * October 2024: Lukas Bartl, LMU München
-  Inference of variable instantiations with Metis
+  Inference of variable instantiations with Metis.
 
 * April - October 2024: Thomas Lindae and Fabian Huch, TU München
   Improvements to the language server for Isabelle/VSCode.
diff -r fcc7a78b7220 -r 0b088316b8a3 COPYRIGHT
--- a/COPYRIGHT	Thu Jan 02 12:14:51 2025 +0100
+++ b/COPYRIGHT	Thu Jan 02 12:49:39 2025 +0100
@@ -1,6 +1,6 @@
 ISABELLE COPYRIGHT NOTICE, LICENCE AND DISCLAIMER.
 
-Copyright (c) 1986-2024,
+Copyright (c) 1986-2025,
   University of Cambridge,
   Technische Universitaet Muenchen,
   and contributors.
diff -r fcc7a78b7220 -r 0b088316b8a3 NEWS
--- a/NEWS	Thu Jan 02 12:14:51 2025 +0100
+++ b/NEWS	Thu Jan 02 12:49:39 2025 +0100
@@ -240,7 +240,9 @@
     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"
+* 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...)
@@ -286,10 +288,9 @@
 Import "HOL-Library.Divides" and keep an eye 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.
+* 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.
 
 
 *** ML ***