# HG changeset patch
# User wenzelm
# Date 1730484700 -3600
# Node ID 42b9bd119d2b769577edab7b2891f8b8cd8822f7
# Parent  e85b5f7f9b164beec3daa1382ee56245989b2417
tuned whitespace;

diff -r e85b5f7f9b16 -r 42b9bd119d2b src/HOL/Library/AList.thy
--- 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'"