| changeset 69790 | 154cf64e403e |
| parent 69785 | 9e326f6f8a24 |
| child 69791 | 195aeee8b30a |
--- 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"