# HG changeset patch
# User traytel
# Date 1554663922 -7200
# Node ID 36821db2e356512e2417fdd04d2d45e3d423799a
# Parent  66dad580507980fda7249041aec73eef9927ad8f
NEWS

diff -r 66dad5805079 -r 36821db2e356 NEWS
--- a/NEWS	Sun Apr 07 20:02:15 2019 +0200
+++ b/NEWS	Sun Apr 07 21:05:22 2019 +0200
@@ -219,6 +219,10 @@
 * Theory HOL-Library.Multiset: the <Union># operator now has the same
 precedence as any other prefix function symbol.
 
+* Theory HOL-Library.Cardinal_Notations has been discontinued in favor
+of the bundle cardinal_syntax (available in Main).
+Minor INCOMPATIBILITY.
+
 * Session HOL-Library and HOL-Number_Theory: Exponentiation by squaring,
 used for computing powers in class "monoid_mult" and modular
 exponentiation.