--- a/NEWS Sun Nov 02 20:36:24 2025 +0100
+++ b/NEWS Mon Nov 03 18:52:06 2025 +0100
@@ -191,6 +191,12 @@
could yield false positives due to incomplete handling of polymorphism
in certain situations; this is now corrected.
+* More efficient default implementation for
+HOL-Library.Discrete_Functions.floor_sqrt.
+
+* More efficient default implementation for "prime" predicate on types nat
+and int.
+
* Theory "HOL.Nat": Added Kleene's Fixed Point Theorem for lfp.
* Theory "HOL-Library.Code_Target_Bit_Shifts" incorporated into