changeset 36622 | e393a91f86df |
parent 36275 | c6ca9e258269 |
child 36851 | 5135adb33157 |
--- a/src/HOL/List.thy Mon May 03 07:59:51 2010 +0200 +++ b/src/HOL/List.thy Tue Apr 20 17:58:34 2010 +0200 @@ -3039,6 +3039,9 @@ lemma length_replicate [simp]: "length (replicate n x) = n" by (induct n) auto +lemma Ex_list_of_length: "\<exists>xs. length xs = n" +by (rule exI[of _ "replicate n undefined"]) simp + lemma map_replicate [simp]: "map f (replicate n x) = replicate n (f x)" by (induct n) auto