NEWS
changeset 81713 378b9d6c52b2
parent 81711 a55b236f9e1d
child 81721 65dd50addc29
equal deleted inserted replaced
81712:97987036f051 81713:378b9d6c52b2
   222 
   222 
   223 *** HOL ***
   223 *** HOL ***
   224 
   224 
   225 * Code generator: command 'code_reserved' now uses parentheses for
   225 * Code generator: command 'code_reserved' now uses parentheses for
   226 target languages, similar to 'code_printing'.
   226 target languages, similar to 'code_printing'.
       
   227 
       
   228 * Theory HOL-Library.Code_Target_Bit_Shifts implemented bit shifts on numeric
       
   229 types by target-language operations; this is also used by
       
   230 HOL-Library.Code_Target_Numeral.
   227 
   231 
   228 * Sledgehammer:
   232 * Sledgehammer:
   229   - Update of bundled provers:
   233   - Update of bundled provers:
   230       . E 3.1 -- with patch on Windows/Cygwin for proper interrupts
   234       . E 3.1 -- with patch on Windows/Cygwin for proper interrupts
   231   - Added instantiations of facts using the "of" attribute
   235   - Added instantiations of facts using the "of" attribute