diff -r 8efec8da78f9 -r 3d518681bb6c NEWS --- a/NEWS Fri Jan 24 10:34:21 2025 +0100 +++ b/NEWS Fri Jan 24 10:48:28 2025 +0100 @@ -231,6 +231,8 @@ * Code generator: command 'code_reserved' now uses parentheses for target languages, similar to 'code_printing'. +* Theory HOL.List: overloaded power operator (^^) on type list. + * Theory HOL-Library.Code_Target_Bit_Shifts implemented bit shifts on numeric types by target-language operations; this is also used by HOL-Library.Code_Target_Numeral.