diff -r 2c3e5e58d93f -r 154cf64e403e NEWS
--- a/NEWS	Mon Feb 04 16:01:44 2019 +0100
+++ b/NEWS	Mon Feb 04 15:39:37 2019 +0100
@@ -87,6 +87,8 @@
 
 *** HOL ***
 
+* exponentiation by squaring in HOL-Library; used for computing powers in monoid_mult and modular exponentiation in HOL-Number_Theory
+
 * more material on residue rings in HOL-Number_Theory:
 Carmichael's function, primitive roots, more properties for "ord"