src/HOL/Code_Numeral.thy
changeset 81706 7beb0cf38292
parent 81681 bac9b067c768
child 81712 97987036f051
--- a/src/HOL/Code_Numeral.thy	Thu Jan 02 08:37:52 2025 +0100
+++ b/src/HOL/Code_Numeral.thy	Thu Jan 02 08:37:55 2025 +0100
@@ -780,7 +780,8 @@
 
 subsection \<open>Serializer setup for target language integers\<close>
 
-code_reserved Eval int Integer abs
+code_reserved
+  (Eval) int Integer abs
 
 code_printing
   type_constructor integer \<rightharpoonup>