| changeset 54849 | d325c7c4a4f7 |
| parent 54848 | a303daddebbf |
| child 54854 | 3324a0078636 |
--- 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