# HG changeset patch
# User haftmann
# Date 1387805062 -3600
# Node ID d325c7c4a4f7c62f412b2cd7c78d4e1dda6119e1
# Parent  a303daddebbf7c75b41ee47520ad8528944100b4
dropped redundant lemma

diff -r a303daddebbf -r d325c7c4a4f7 src/HOL/Word/Word.thy
--- a/src/HOL/Word/Word.thy	Mon Dec 23 14:24:21 2013 +0100
+++ b/src/HOL/Word/Word.thy	Mon Dec 23 14:24:22 2013 +0100
@@ -4010,9 +4010,6 @@
 
 subsubsection "map, map2, commuting with rotate(r)"
 
-lemma last_map: "xs ~= [] \<Longrightarrow> last (map f xs) = f (last xs)"
-  by (induct xs) auto
-
 lemma butlast_map:
   "xs ~= [] \<Longrightarrow> butlast (map f xs) = map f (butlast xs)"
   by (induct xs) auto