changeset 81708 | fcc7a78b7220 |
parent 81706 | 7beb0cf38292 |
child 81709 | 0b088316b8a3 |
--- a/NEWS Thu Jan 02 12:13:18 2025 +0100 +++ b/NEWS Thu Jan 02 12:14:51 2025 +0100 @@ -222,8 +222,8 @@ *** HOL *** -* Code generator: `code_reserved` now uses brackets for target languages, -similar to `code_printing. +* Code generator: command 'code_reserved' now uses parentheses for +target languages, similar to 'code_printing'. * Sledgehammer: - Added instantiations of facts using the "of" attribute