--- 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.
--- 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.
--- 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 ***