# HG changeset patch
# User wenzelm
# Date 1738009871 -3600
# Node ID e6f5434ad95a6254c7163879dcf93ffb5d389660
# Parent  d67dadd69d072a3d0f8d35a576c2caed993ab7ff
more NEWS;

diff -r d67dadd69d07 -r e6f5434ad95a NEWS
--- a/NEWS	Mon Jan 27 21:31:02 2025 +0100
+++ b/NEWS	Mon Jan 27 21:31:11 2025 +0100
@@ -130,6 +130,20 @@
 commands, which need to copy mixfix declarations from elsewhere and thus
 break after changes in the library.
 
+* Former theory "HOL-Library.Adhoc_Overloading" is now included in Pure,
+with a few changes (minor INCOMPATIBILITY):
+
+  - Theory imports of "HOL-Library.Adhoc_Overloading" need to be removed
+    (or replaced by Main).
+
+  - Equivalence of overloaded constants has become more liberal: sorts
+    of type variables are ignore, schematic type variables only need to
+    match (in both directions) instead of being literally equal.
+
+  - Command syntax now requires a separator: "adhoc_overloading c \<rightleftharpoons> vs".
+
+  - The "no" keyword for bundles works as for 'syntax' / 'no_syntax'.
+
 * Theory "HOL-Library.Datatype_Records" provides bundle
 "datatype_record_syntax" to exchange its alternative notation versus
 regular "record_syntax". This also allows to swap record syntax later