# HG changeset patch
# User wenzelm
# Date 1737712108 -3600
# Node ID 3d518681bb6c0e0dcb97649f9228e714eb001970
# Parent  8efec8da78f91586876cd46c07221f36013cbe94
more NEWS;

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.