equal
deleted
inserted
replaced
228 |
228 |
229 *** HOL *** |
229 *** HOL *** |
230 |
230 |
231 * Code generator: command 'code_reserved' now uses parentheses for |
231 * Code generator: command 'code_reserved' now uses parentheses for |
232 target languages, similar to 'code_printing'. |
232 target languages, similar to 'code_printing'. |
|
233 |
|
234 * Theory HOL.List: overloaded power operator (^^) on type list. |
233 |
235 |
234 * Theory HOL-Library.Code_Target_Bit_Shifts implemented bit shifts on numeric |
236 * Theory HOL-Library.Code_Target_Bit_Shifts implemented bit shifts on numeric |
235 types by target-language operations; this is also used by |
237 types by target-language operations; this is also used by |
236 HOL-Library.Code_Target_Numeral. |
238 HOL-Library.Code_Target_Numeral. |
237 |
239 |