# HG changeset patch
# User nipkow
# Date 1266505706 -3600
# Node ID 2b9bce05e84b848a617f37361c059242e479d2c5
# Parent  5c5457a7be85732b4b209b310ab40621d682f694
added lemma

diff -r 5c5457a7be85 -r 2b9bce05e84b src/HOL/List.thy
--- a/src/HOL/List.thy	Thu Feb 18 08:17:24 2010 +0100
+++ b/src/HOL/List.thy	Thu Feb 18 16:08:26 2010 +0100
@@ -720,6 +720,11 @@
 lemma map_map [simp]: "map f (map g xs) = map (f \<circ> g) xs"
 by (induct xs) auto
 
+lemma map_comp_map[simp]: "((map f) o (map g)) = map(f o g)"
+apply(rule ext)
+apply(simp)
+done
+
 lemma rev_map: "rev (map f xs) = map f (rev xs)"
 by (induct xs) auto