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