NEWS
changeset 70080 36821db2e356
parent 70075 ee0b8e06b01c
child 70082 4f936de6d9b8
child 70087 2d19e7eb027a
     1.1 --- a/NEWS	Sun Apr 07 20:02:15 2019 +0200
     1.2 +++ b/NEWS	Sun Apr 07 21:05:22 2019 +0200
     1.3 @@ -219,6 +219,10 @@
     1.4  * Theory HOL-Library.Multiset: the <Union># operator now has the same
     1.5  precedence as any other prefix function symbol.
     1.6  
     1.7 +* Theory HOL-Library.Cardinal_Notations has been discontinued in favor
     1.8 +of the bundle cardinal_syntax (available in Main).
     1.9 +Minor INCOMPATIBILITY.
    1.10 +
    1.11  * Session HOL-Library and HOL-Number_Theory: Exponentiation by squaring,
    1.12  used for computing powers in class "monoid_mult" and modular
    1.13  exponentiation.