# HG changeset patch
# User nipkow
# Date 1746596887 -7200
# Node ID 6e3e59ac12c94e61a2047dc5f654abbb8bc2c982
# Parent  2f225d5044b54034025ee094ee554da2019343cd
Kleene's fixpoint thm

diff -r 2f225d5044b5 -r 6e3e59ac12c9 NEWS
--- 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.