NEWS
changeset 81813 8df58b532ecb
parent 81796 88c172ebffdd
child 81868 d832c4a676e1
--- a/NEWS	Wed Jan 15 17:48:38 2025 +0100
+++ b/NEWS	Thu Jan 16 09:26:56 2025 +0100
@@ -235,6 +235,9 @@
 types by target-language operations; this is also used by
 HOL-Library.Code_Target_Numeral.
 
+* Theory HOL-Library.Code_Bit_Shifts_for_Arithmetic rewrites certain
+arithmetic operations on numerals to bit shifts.
+
 * Sledgehammer:
   - Update of bundled provers:
       . E 3.1 -- with patch on Windows/Cygwin for proper interrupts