diff -r 53fea2ccab19 -r 7beb0cf38292 src/HOL/Imperative_HOL/Array.thy --- a/src/HOL/Imperative_HOL/Array.thy Thu Jan 02 08:37:52 2025 +0100 +++ b/src/HOL/Imperative_HOL/Array.thy Thu Jan 02 08:37:55 2025 +0100 @@ -451,7 +451,7 @@ code_printing constant Array.upd' \ (SML) "(fn/ ()/ =>/ Array.update/ ((_),/ IntInf.toInt _,/ (_)))" code_printing constant "HOL.equal :: 'a array \ 'a array \ bool" \ (SML) infixl 6 "=" -code_reserved SML Array +code_reserved (SML) Array text \OCaml\ @@ -467,7 +467,7 @@ code_printing constant Array.upd' \ (OCaml) "(fun/ ()/ ->/ Array.set/ _/ (Z.to'_int/ _)/ _)" code_printing constant "HOL.equal :: 'a array \ 'a array \ bool" \ (OCaml) infixl 4 "=" -code_reserved OCaml Array +code_reserved (OCaml) Array text \Haskell\