--- a/src/HOL/HOLCF/Map_Functions.thy Sun Dec 19 09:52:33 2010 -0800
+++ b/src/HOL/HOLCF/Map_Functions.thy Sun Dec 19 10:33:46 2010 -0800
@@ -191,6 +191,9 @@
lemma u_map_map: "u_map\<cdot>f\<cdot>(u_map\<cdot>g\<cdot>p) = u_map\<cdot>(\<Lambda> x. f\<cdot>(g\<cdot>x))\<cdot>p"
by (induct p) simp_all
+lemma u_map_oo: "u_map\<cdot>(f oo g) = u_map\<cdot>f oo u_map\<cdot>g"
+by (simp add: cfcomp1 u_map_map eta_cfun)
+
lemma ep_pair_u_map: "ep_pair e p \<Longrightarrow> ep_pair (u_map\<cdot>e) (u_map\<cdot>p)"
apply default
apply (case_tac x, simp, simp add: ep_pair.e_inverse)