NEWS
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