NEWS
changeset 81713 378b9d6c52b2
parent 81711 a55b236f9e1d
child 81721 65dd50addc29
--- a/NEWS	Sat Jan 04 14:25:56 2025 +0100
+++ b/NEWS	Sat Jan 04 14:41:30 2025 +0100
@@ -225,6 +225,10 @@
 * Code generator: command 'code_reserved' now uses parentheses for
 target languages, similar to 'code_printing'.
 
+* 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.
+
 * Sledgehammer:
   - Update of bundled provers:
       . E 3.1 -- with patch on Windows/Cygwin for proper interrupts