Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Library/AList.thy
changeset 81306 42b9bd119d2b
parent 74157 8e2355ddce1b 
--- 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'"
isabelle