changeset 81706 | 7beb0cf38292 |
parent 81704 | 9253dadbd4ac |
child 81708 | fcc7a78b7220 |
--- a/NEWS Thu Jan 02 08:37:52 2025 +0100 +++ b/NEWS Thu Jan 02 08:37:55 2025 +0100 @@ -222,6 +222,9 @@ *** HOL *** +* Code generator: `code_reserved` now uses brackets for target languages, +similar to `code_printing. + * Sledgehammer: - Added instantiations of facts using the "of" attribute (e.g. "assms(1)[of x]"), which can be activated using the