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>