merged
authornipkow
Wed, 12 May 2021 06:35:16 +0200
changeset 73935 71c45d60a90a
parent 73934 73c50ce808ed (current diff)
parent 73931 78929c029785 (diff)
child 73936 50437744eb1c
child 73941 a63d76ba0a03
merged
--- 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 \<open>\<open>map_ran\<close>\<close>
 
-definition map_ran :: "('key \<Rightarrow> 'val \<Rightarrow> 'val) \<Rightarrow> ('key \<times> 'val) list \<Rightarrow> ('key \<times> 'val) list"
+definition map_ran :: "('key \<Rightarrow> 'val1 \<Rightarrow> 'val2) \<Rightarrow> ('key \<times> 'val1) list \<Rightarrow> ('key \<times> 'val2) list"
   where "map_ran f = map (\<lambda>(k, v). (k, f k v))"
 
 lemma map_ran_simps [simp]: