# HG changeset patch
# User kleing
# Date 1194403877 -3600
# Node ID e2eac0c30ff5a7cb7a0ea81e84f369addd0473d4
# Parent  e34b2265698a1e84ad5f7d64b8d08d7fd2cd80c5
map and prefix

diff -r e34b2265698a -r e2eac0c30ff5 src/HOL/Library/List_Prefix.thy
--- 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)