src/HOL/Fun.thy
changeset 40968 a6fcd305f7dc
parent 40719 acb830207103
child 40969 fb2d3ccda5a7
equal deleted inserted replaced
40965:54b6c9e1c157 40968:a6fcd305f7dc
   124 
   124 
   125 lemma map_fun_apply [simp]:
   125 lemma map_fun_apply [simp]:
   126   "map_fun f g h x = g (h (f x))"
   126   "map_fun f g h x = g (h (f x))"
   127   by (simp add: map_fun_def)
   127   by (simp add: map_fun_def)
   128 
   128 
   129 type_mapper map_fun
   129 type_lifting map_fun
   130   by (simp_all add: fun_eq_iff)
   130   by (simp_all add: fun_eq_iff)
   131 
   131 
   132 
   132 
   133 subsection {* Injectivity and Bijectivity *}
   133 subsection {* Injectivity and Bijectivity *}
   134 
   134