Kleene's fixpoint thm

--- a/NEWS	Wed May 07 06:21:46 2025 +0200
+++ b/NEWS	Wed May 07 07:48:07 2025 +0200
@@ -71,6 +71,8 @@
 yield false positives due to incomplete handling of polymorphism in certain
 situations; this is now corrected.
 
+* Theory "HOL.Nat": Added Kleene's Fixed Point Theorem for lfp.
+
 * Theory "HOL-Library.Code_Target_Bit_Shifts" incorporated into HOL-Main.
 Minor INCOMPATIBILITY.