Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
NEWS
authorhaftmann
Mon, 14 Apr 2025 20:19:05 +0200
changeset 82505 fa641833c0ff
parent 82504 3034e6fd9de4
child 82506 289b18955960
NEWS
NEWS file | annotate | diff | comparison | revisions 
--- a/NEWS	Mon Apr 14 20:19:05 2025 +0200
+++ b/NEWS	Mon Apr 14 20:19:05 2025 +0200
@@ -40,6 +40,10 @@
 
 *** HOL ***
 
+* Normalization by evaluation (method "normalization", command value) could
+yield false positives due to incomplete handling of polymorphism in certain
+situations; this is now corrected.
+
 * Theory "HOL-Library.Code_Target_Bit_Shifts" incorporated into HOL-Main.
 Minor INCOMPATIBILITY.
isabelle