# HG changeset patch # User nipkow # Date 1620794116 -7200 # Node ID 71c45d60a90a0d937243d7143a655d5bd24ad447 # Parent 73c50ce808ed90284ddaa61662ea6f5102931770# Parent 78929c029785260003aae44bd5e1d70ce6f83754 merged diff -r 73c50ce808ed -r 71c45d60a90a src/HOL/Library/AList.thy --- a/src/HOL/Library/AList.thy Tue May 11 21:57:43 2021 +0200 +++ b/src/HOL/Library/AList.thy Wed May 12 06:35:16 2021 +0200 @@ -475,7 +475,7 @@ subsection \\map_ran\\ -definition map_ran :: "('key \ 'val \ 'val) \ ('key \ 'val) list \ ('key \ 'val) list" +definition map_ran :: "('key \ 'val1 \ 'val2) \ ('key \ 'val1) list \ ('key \ 'val2) list" where "map_ran f = map (\(k, v). (k, f k v))" lemma map_ran_simps [simp]: