map and prefix

--- a/src/HOL/Library/List_Prefix.thy	Tue Nov 06 22:50:39 2007 +0100
+++ b/src/HOL/Library/List_Prefix.thy	Wed Nov 07 03:51:17 2007 +0100
@@ -162,6 +162,10 @@
   apply simp
   done
 
+lemma map_prefixI: 
+  "xs \<le> ys \<Longrightarrow> map f xs \<le> map f ys"
+  by (clarsimp simp: prefix_def)
+
 lemma prefix_length_less:
   "xs < ys \<Longrightarrow> length xs < length ys"
   apply (clarsimp simp: strict_prefix_def)