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