# 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 ~= [] \ last (map f xs) = f (last xs)" - by (induct xs) auto - lemma butlast_map: "xs ~= [] \ butlast (map f xs) = map f (butlast xs)" by (induct xs) auto