author | haftmann |
Mon, 23 Dec 2013 14:24:22 +0100 | |
changeset 54849 | d325c7c4a4f7 |
parent 54848 | a303daddebbf |
child 54850 | 980817309b78 |
--- 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