# HG changeset patch
# User haftmann
# Date 1762192326 -3600
# Node ID bcc1001cbfbda98bcf81dcc5d1d592a20439f421
# Parent  791c44b1d130abd854414f96b8210e66d5e12aa3
NEWS

diff -r 791c44b1d130 -r bcc1001cbfbd NEWS
--- 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