--- a/src/HOL/Library/IArray.thy Fri Sep 20 19:07:10 2024 +0200
+++ b/src/HOL/Library/IArray.thy Fri Sep 20 19:51:08 2024 +0200
@@ -28,7 +28,7 @@
qualified definition of_fun :: "(nat \<Rightarrow> 'a) \<Rightarrow> nat \<Rightarrow> 'a iarray" where
[simp]: "of_fun f n = IArray (map f [0..<n])"
-qualified definition sub :: "'a iarray \<Rightarrow> nat \<Rightarrow> 'a" (infixl "!!" 100) where
+qualified definition sub :: "'a iarray \<Rightarrow> nat \<Rightarrow> 'a" (infixl \<open>!!\<close> 100) where
[simp]: "as !! n = IArray.list_of as ! n"
qualified definition length :: "'a iarray \<Rightarrow> nat" where