--- a/NEWS Mon May 04 17:35:29 2020 +0200
+++ b/NEWS Wed May 13 12:55:33 2020 +0200
@@ -35,6 +35,9 @@
*** HOL ***
+* New constant "power_int" for exponentiation with integer exponent,
+written as "x powi n".
+
* Added the "at most 1" quantifier, Uniq.
* For the natural numbers, Sup{} = 0.