author | wenzelm |
Fri, 24 Jan 2025 10:48:28 +0100 | |
changeset 81965 | 3d518681bb6c |
parent 81964 | 8efec8da78f9 |
child 81966 | 6d34097215be |
--- 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.