--- a/src/HOL/Library/AList.thy Fri Nov 01 18:55:47 2024 +0100
+++ b/src/HOL/Library/AList.thy Fri Nov 01 19:11:40 2024 +0100
@@ -25,7 +25,7 @@
"update k v [] = [(k, v)]"
| "update k v (p # ps) = (if fst p = k then (k, v) # ps else p # update k v ps)"
-lemma update_conv': "map_of (update k v al) = (map_of al)(k\<mapsto>v)"
+lemma update_conv': "map_of (update k v al) = (map_of al)(k\<mapsto>v)"
by (induct al) (auto simp add: fun_eq_iff)
corollary update_conv: "map_of (update k v al) k' = ((map_of al)(k\<mapsto>v)) k'"